[STATEMENT]
lemma subcls_C_Object:
assumes "class": "is_class P C" and wf: "wf_prog wf_md P"
shows "P \<turnstile> C \<preceq>\<^sup>* Object"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> C \<preceq>\<^sup>* Object
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> C \<preceq>\<^sup>* Object
[PROOF STEP]
using wf "class"
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
is_class P C

goal (1 subgoal):
 1. P \<turnstile> C \<preceq>\<^sup>* Object
[PROOF STEP]
proof(induct rule: subcls1_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<turnstile> Object \<preceq>\<^sup>* Object
 2. \<And>C D. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; P \<turnstile> D \<preceq>\<^sup>* Object\<rbrakk> \<Longrightarrow> P \<turnstile> C \<preceq>\<^sup>* Object
[PROOF STEP]
case Subcls
[PROOF STATE]
proof (state)
this:
C_ \<noteq> Object
P \<turnstile> C_ \<prec>\<^sup>1 D_
is_class P D_
P \<turnstile> D_ \<preceq>\<^sup>* Object

goal (2 subgoals):
 1. P \<turnstile> Object \<preceq>\<^sup>* Object
 2. \<And>C D. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; P \<turnstile> D \<preceq>\<^sup>* Object\<rbrakk> \<Longrightarrow> P \<turnstile> C \<preceq>\<^sup>* Object
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C_ \<noteq> Object
P \<turnstile> C_ \<prec>\<^sup>1 D_
is_class P D_
P \<turnstile> D_ \<preceq>\<^sup>* Object
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
C_ \<noteq> Object
P \<turnstile> C_ \<prec>\<^sup>1 D_
is_class P D_
P \<turnstile> D_ \<preceq>\<^sup>* Object

goal (1 subgoal):
 1. P \<turnstile> C_ \<preceq>\<^sup>* Object
[PROOF STEP]
by(simp add: converse_rtrancl_into_rtrancl)
[PROOF STATE]
proof (state)
this:
P \<turnstile> C_ \<preceq>\<^sup>* Object

goal (1 subgoal):
 1. P \<turnstile> Object \<preceq>\<^sup>* Object
[PROOF STEP]
qed fast


[STATEMENT]
lemma is_type_pTs:
assumes "wf_prog wf_md P" and "(C,S,fs,ms) \<in> set P" and "(M,b,Ts,T,m) \<in> set ms"
shows "set Ts \<subseteq> types P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set Ts \<subseteq> types P
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set Ts \<subseteq> types P
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set Ts \<Longrightarrow> x \<in> types P
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
wf_prog wf_md P
(C, S, fs, ms) \<in> set P
(M, b, Ts, T, m) \<in> set ms
[PROOF STEP]
have "wf_mdecl wf_md P C (M,b,Ts,T,m)"
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
(C, S, fs, ms) \<in> set P
(M, b, Ts, T, m) \<in> set ms

goal (1 subgoal):
 1. wf_mdecl wf_md P C (M, b, Ts, T, m)
[PROOF STEP]
by (unfold wf_prog_def wf_cdecl_def) auto
[PROOF STATE]
proof (state)
this:
wf_mdecl wf_md P C (M, b, Ts, T, m)

goal (1 subgoal):
 1. \<And>x. x \<in> set Ts \<Longrightarrow> x \<in> types P
[PROOF STEP]
hence "\<forall>t \<in> set Ts. is_type P t"
[PROOF STATE]
proof (prove)
using this:
wf_mdecl wf_md P C (M, b, Ts, T, m)

goal (1 subgoal):
 1. \<forall>t\<in>set Ts. is_type P t
[PROOF STEP]
by (unfold wf_mdecl_def) auto
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set Ts. is_type P t

goal (1 subgoal):
 1. \<And>x. x \<in> set Ts \<Longrightarrow> x \<in> types P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set Ts. is_type P t

goal (1 subgoal):
 1. \<And>x. x \<in> set Ts \<Longrightarrow> x \<in> types P
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set Ts \<Longrightarrow> x \<in> types P
[PROOF STEP]
assume "t \<in> set Ts"
[PROOF STATE]
proof (state)
this:
t \<in> set Ts

goal (1 subgoal):
 1. \<And>x. x \<in> set Ts \<Longrightarrow> x \<in> types P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>set Ts. is_type P t
t \<in> set Ts
[PROOF STEP]
have "is_type P t"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>set Ts. is_type P t
t \<in> set Ts

goal (1 subgoal):
 1. is_type P t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_type P t

goal (1 subgoal):
 1. \<And>x. x \<in> set Ts \<Longrightarrow> x \<in> types P
[PROOF STEP]
thus "t \<in> types P"
[PROOF STATE]
proof (prove)
using this:
is_type P t

goal (1 subgoal):
 1. t \<in> types P
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
t \<in> types P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_supercls_distinct_app:
assumes wf:"wf_prog wf_md P"
  and nObj: "C \<noteq> Object" and cls: "class P C = \<lfloor>(D, fs, ms)\<rfloor>"
  and super: "supercls_lst P (C#Cs)" and dist: "distinct (C#Cs)"
shows "distinct (D#C#Cs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (D # C # Cs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct (D # C # Cs)
[PROOF STEP]
have "\<not> P \<turnstile> D \<preceq>\<^sup>* C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (D, C) \<notin> (subcls1 P)\<^sup>*
[PROOF STEP]
using subcls1_wfD[OF subcls1I[OF cls nObj] wf]
[PROOF STATE]
proof (prove)
using this:
D \<noteq> C \<and> (D, C) \<notin> (subcls1 P)\<^sup>+

goal (1 subgoal):
 1. (D, C) \<notin> (subcls1 P)\<^sup>*
[PROOF STEP]
by (simp add: rtrancl_eq_or_trancl)
[PROOF STATE]
proof (state)
this:
(D, C) \<notin> (subcls1 P)\<^sup>*

goal (1 subgoal):
 1. distinct (D # C # Cs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(D, C) \<notin> (subcls1 P)\<^sup>*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(D, C) \<notin> (subcls1 P)\<^sup>*

goal (1 subgoal):
 1. distinct (D # C # Cs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(D, C) \<notin> (subcls1 P)\<^sup>*
wf_prog wf_md P
C \<noteq> Object
class P C = \<lfloor>(D, fs, ms)\<rfloor>
supercls_lst P (C # Cs)
distinct (C # Cs)

goal (1 subgoal):
 1. distinct (D # C # Cs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (D # C # Cs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sees_wf_mdecl:
assumes wf: "wf_prog wf_md P" and sees: "P \<turnstile> C sees M,b:Ts\<rightarrow>T = m in D"
shows "wf_mdecl wf_md P D (M,b,Ts,T,m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_mdecl wf_md P D (M, b, Ts, T, m)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_mdecl wf_md P D (M, b, Ts, T, m)
[PROOF STEP]
using wf visible_method_exists[OF sees]
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
\<exists>D' fs ms. class P D = \<lfloor>(D', fs, ms)\<rfloor> \<and> map_of ms M = \<lfloor>(b, Ts, T, m)\<rfloor>

goal (1 subgoal):
 1. wf_mdecl wf_md P D (M, b, Ts, T, m)
[PROOF STEP]
proof(cases b)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>wf_prog wf_md P; \<exists>D' fs ms. class P D = \<lfloor>(D', fs, ms)\<rfloor> \<and> map_of ms M = \<lfloor>(b, Ts, T, m)\<rfloor>; b = Static\<rbrakk> \<Longrightarrow> wf_mdecl wf_md P D (M, b, Ts, T, m)
 2. \<lbrakk>wf_prog wf_md P; \<exists>D' fs ms. class P D = \<lfloor>(D', fs, ms)\<rfloor> \<and> map_of ms M = \<lfloor>(b, Ts, T, m)\<rfloor>; b = NonStatic\<rbrakk> \<Longrightarrow> wf_mdecl wf_md P D (M, b, Ts, T, m)
[PROOF STEP]
qed (fastforce simp:wf_cdecl_def dest!:class_wf dest:map_of_SomeD)+


[STATEMENT]
lemma sees_method_mono [rule_format (no_asm)]:
assumes sub: "P \<turnstile> C' \<preceq>\<^sup>* C" and wf: "wf_prog wf_md P"
shows "\<forall>D b Ts T m. P \<turnstile> C sees M,b:Ts\<rightarrow>T = m in D \<longrightarrow>
     (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M,b:Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)"
(*<*)
  (is "\<forall>D b Ts T m. ?P C D b Ts T m \<longrightarrow> ?Q C' D b Ts T m")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>D b Ts T m. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
proof(rule disjE[OF rtranclD[OF sub]])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. C' = C \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
 2. C' \<noteq> C \<and> (C', C) \<in> (subcls1 P)\<^sup>+ \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
assume "C' = C"
[PROOF STATE]
proof (state)
this:
C' = C

goal (2 subgoals):
 1. C' = C \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
 2. C' \<noteq> C \<and> (C', C) \<in> (subcls1 P)\<^sup>+ \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C' = C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C' = C

goal (1 subgoal):
 1. \<forall>D b Ts T m. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C' = C
P \<turnstile> C' \<preceq>\<^sup>* C
wf_prog wf_md P

goal (1 subgoal):
 1. \<forall>D b Ts T m. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>D b Ts T m. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)

goal (1 subgoal):
 1. C' \<noteq> C \<and> (C', C) \<in> (subcls1 P)\<^sup>+ \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C' \<noteq> C \<and> (C', C) \<in> (subcls1 P)\<^sup>+ \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
assume "C' \<noteq> C \<and> (C', C) \<in> (subcls1 P)\<^sup>+"
[PROOF STATE]
proof (state)
this:
C' \<noteq> C \<and> (C', C) \<in> (subcls1 P)\<^sup>+

goal (1 subgoal):
 1. C' \<noteq> C \<and> (C', C) \<in> (subcls1 P)\<^sup>+ \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C' \<noteq> C \<and> (C', C) \<in> (subcls1 P)\<^sup>+
[PROOF STEP]
have neq: "C' \<noteq> C" and subcls1: "(C', C) \<in> (subcls1 P)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
C' \<noteq> C \<and> (C', C) \<in> (subcls1 P)\<^sup>+

goal (1 subgoal):
 1. C' \<noteq> C &&& (C', C) \<in> (subcls1 P)\<^sup>+
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
C' \<noteq> C
(C', C) \<in> (subcls1 P)\<^sup>+

goal (1 subgoal):
 1. C' \<noteq> C \<and> (C', C) \<in> (subcls1 P)\<^sup>+ \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>D b Ts T m. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
proof(induct rule: trancl_trans_induct[OF subcls1])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. P \<turnstile> x \<prec>\<^sup>1 y \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
 2. \<And>x y z. \<lbrakk>(x, y) \<in> (subcls1 P)\<^sup>+; \<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T); (y, z) \<in> (subcls1 P)\<^sup>+; \<forall>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> y sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)\<rbrakk> \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
case (2 x y z)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (subcls1 P)\<^sup>+
\<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
(y, z) \<in> (subcls1 P)\<^sup>+
\<forall>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> y sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)

goal (2 subgoals):
 1. \<And>x y. P \<turnstile> x \<prec>\<^sup>1 y \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
 2. \<And>x y z. \<lbrakk>(x, y) \<in> (subcls1 P)\<^sup>+; \<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T); (y, z) \<in> (subcls1 P)\<^sup>+; \<forall>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> y sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)\<rbrakk> \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> (subcls1 P)\<^sup>+
\<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
(y, z) \<in> (subcls1 P)\<^sup>+
\<forall>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> y sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
have zy: "\<And>D b Ts T m. ?P z D b Ts T m \<Longrightarrow> ?Q y D b Ts T m"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> (subcls1 P)\<^sup>+
\<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
(y, z) \<in> (subcls1 P)\<^sup>+
\<forall>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> y sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)

goal (1 subgoal):
 1. \<And>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> y sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<turnstile> z sees M, ?b :  ?Ts\<rightarrow>?T = ?m in ?D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> y sees M, ?b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> ?Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> ?T

goal (2 subgoals):
 1. \<And>x y. P \<turnstile> x \<prec>\<^sup>1 y \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
 2. \<And>x y z. \<lbrakk>(x, y) \<in> (subcls1 P)\<^sup>+; \<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T); (y, z) \<in> (subcls1 P)\<^sup>+; \<forall>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> y sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)\<rbrakk> \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
have "\<And>D b Ts T m. ?P z D b Ts T m \<Longrightarrow> ?Q x D b Ts T m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
fix D b Ts T m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
assume P: "?P z D b Ts T m"
[PROOF STATE]
proof (state)
this:
P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D

goal (1 subgoal):
 1. \<And>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D
[PROOF STEP]
show "?Q x D b Ts T m"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D

goal (1 subgoal):
 1. \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
using zy[OF P] 2(2)
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D
\<exists>D' Ts' T' m'. P \<turnstile> y sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
\<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)

goal (1 subgoal):
 1. \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
by(fast elim: widen_trans widens_trans)
[PROOF STATE]
proof (state)
this:
\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<turnstile> z sees M, ?b :  ?Ts\<rightarrow>?T = ?m in ?D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, ?b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> ?Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> ?T

goal (2 subgoals):
 1. \<And>x y. P \<turnstile> x \<prec>\<^sup>1 y \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
 2. \<And>x y z. \<lbrakk>(x, y) \<in> (subcls1 P)\<^sup>+; \<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T); (y, z) \<in> (subcls1 P)\<^sup>+; \<forall>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> y sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)\<rbrakk> \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> z sees M, ?b :  ?Ts\<rightarrow>?T = ?m in ?D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, ?b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> ?Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> ?T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> z sees M, ?b :  ?Ts\<rightarrow>?T = ?m in ?D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, ?b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> ?Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> ?T

goal (1 subgoal):
 1. \<forall>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>D b Ts T m. P \<turnstile> z sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)

goal (1 subgoal):
 1. \<And>x y. P \<turnstile> x \<prec>\<^sup>1 y \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. P \<turnstile> x \<prec>\<^sup>1 y \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
case (1 x y)
[PROOF STATE]
proof (state)
this:
P \<turnstile> x \<prec>\<^sup>1 y

goal (1 subgoal):
 1. \<And>x y. P \<turnstile> x \<prec>\<^sup>1 y \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
have "\<And>D b Ts T m. ?P y D b Ts T m \<Longrightarrow> ?Q x D b Ts T m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
fix D b Ts T m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
assume P: "?P y D b Ts T m"
[PROOF STATE]
proof (state)
this:
P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D

goal (1 subgoal):
 1. \<And>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D
[PROOF STEP]
obtain Mm where sees: "P \<turnstile> y sees_methods Mm" and
                           M: "Mm M = \<lfloor>((b, Ts, T, m), D)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D

goal (1 subgoal):
 1. (\<And>Mm. \<lbrakk>P \<turnstile> y sees_methods Mm; Mm M = \<lfloor>((b, Ts, T, m), D)\<rfloor>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(clarsimp simp:Method_def)
[PROOF STATE]
proof (state)
this:
P \<turnstile> y sees_methods Mm
Mm M = \<lfloor>((b, Ts, T, m), D)\<rfloor>

goal (1 subgoal):
 1. \<And>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
obtain fs ms where nObj: "x \<noteq> Object" and
                         cls: "class P x = \<lfloor>(y, fs, ms)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>fs ms. \<lbrakk>x \<noteq> Object; class P x = \<lfloor>(y, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using subcls1D[OF 1]
[PROOF STATE]
proof (prove)
using this:
x \<noteq> Object \<and> (\<exists>fs ms. class P x = \<lfloor>(y, fs, ms)\<rfloor>)

goal (1 subgoal):
 1. (\<And>fs ms. \<lbrakk>x \<noteq> Object; class P x = \<lfloor>(y, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
x \<noteq> Object
class P x = \<lfloor>(y, fs, ms)\<rfloor>

goal (1 subgoal):
 1. \<And>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
have x_meth: "P \<turnstile> x sees_methods Mm ++ (map_option (\<lambda>m. (m, x)) \<circ> map_of ms)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> x sees_methods Mm ++ (map_option (\<lambda>m. (m, x)) \<circ> map_of ms)
[PROOF STEP]
using sees_methods_rec[OF cls nObj sees]
[PROOF STATE]
proof (prove)
using this:
?Mm' = Mm ++ (map_option (\<lambda>m. (m, x)) \<circ> map_of ms) \<Longrightarrow> P \<turnstile> x sees_methods ?Mm'

goal (1 subgoal):
 1. P \<turnstile> x sees_methods Mm ++ (map_option (\<lambda>m. (m, x)) \<circ> map_of ms)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<turnstile> x sees_methods Mm ++ (map_option (\<lambda>m. (m, x)) \<circ> map_of ms)

goal (1 subgoal):
 1. \<And>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
show "?Q x D b Ts T m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
proof(cases "map_of ms M")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. map_of ms M = None \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
 2. \<And>a. map_of ms M = \<lfloor>a\<rfloor> \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
map_of ms M = None

goal (2 subgoals):
 1. map_of ms M = None \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
 2. \<And>a. map_of ms M = \<lfloor>a\<rfloor> \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map_of ms M = None
[PROOF STEP]
have "\<exists>m'. P \<turnstile> x sees M, b :  Ts\<rightarrow>T = m' in D"
[PROOF STATE]
proof (prove)
using this:
map_of ms M = None

goal (1 subgoal):
 1. \<exists>m'. P \<turnstile> x sees M, b :  Ts\<rightarrow>T = m' in D
[PROOF STEP]
using M x_meth
[PROOF STATE]
proof (prove)
using this:
map_of ms M = None
Mm M = \<lfloor>((b, Ts, T, m), D)\<rfloor>
P \<turnstile> x sees_methods Mm ++ (map_option (\<lambda>m. (m, x)) \<circ> map_of ms)

goal (1 subgoal):
 1. \<exists>m'. P \<turnstile> x sees M, b :  Ts\<rightarrow>T = m' in D
[PROOF STEP]
by(fastforce simp add:Method_def map_add_def split:option.split)
[PROOF STATE]
proof (state)
this:
\<exists>m'. P \<turnstile> x sees M, b :  Ts\<rightarrow>T = m' in D

goal (2 subgoals):
 1. map_of ms M = None \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
 2. \<And>a. map_of ms M = \<lfloor>a\<rfloor> \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m'. P \<turnstile> x sees M, b :  Ts\<rightarrow>T = m' in D
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>m'. P \<turnstile> x sees M, b :  Ts\<rightarrow>T = m' in D

goal (1 subgoal):
 1. \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T

goal (1 subgoal):
 1. \<And>a. map_of ms M = \<lfloor>a\<rfloor> \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. map_of ms M = \<lfloor>a\<rfloor> \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
case (Some a)
[PROOF STATE]
proof (state)
this:
map_of ms M = \<lfloor>a\<rfloor>

goal (1 subgoal):
 1. \<And>a. map_of ms M = \<lfloor>a\<rfloor> \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map_of ms M = \<lfloor>a\<rfloor>
[PROOF STEP]
obtain b' Ts' T' m' where a: "a = (b',Ts',T',m')"
[PROOF STATE]
proof (prove)
using this:
map_of ms M = \<lfloor>a\<rfloor>

goal (1 subgoal):
 1. (\<And>b' Ts' T' m'. a = (b', Ts', T', m') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases a)
[PROOF STATE]
proof (state)
this:
a = (b', Ts', T', m')

goal (1 subgoal):
 1. \<And>a. map_of ms M = \<lfloor>a\<rfloor> \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = (b', Ts', T', m')
[PROOF STEP]
have "(\<exists>m' Mm. P \<turnstile> y sees_methods Mm \<and> Mm M = \<lfloor>((b, Ts, T, m'), D)\<rfloor>)
              \<longrightarrow> b' = b \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T"
[PROOF STATE]
proof (prove)
using this:
a = (b', Ts', T', m')

goal (1 subgoal):
 1. (\<exists>m' Mm. P \<turnstile> y sees_methods Mm \<and> Mm M = \<lfloor>((b, Ts, T, m'), D)\<rfloor>) \<longrightarrow> b' = b \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
using nObj class_wf[OF cls wf] map_of_SomeD[OF Some]
[PROOF STATE]
proof (prove)
using this:
a = (b', Ts', T', m')
x \<noteq> Object
wf_cdecl wf_md P (x, y, fs, ms)
(M, a) \<in> set ms

goal (1 subgoal):
 1. (\<exists>m' Mm. P \<turnstile> y sees_methods Mm \<and> Mm M = \<lfloor>((b, Ts, T, m'), D)\<rfloor>) \<longrightarrow> b' = b \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
by(clarsimp simp: wf_cdecl_def Method_def) fast
[PROOF STATE]
proof (state)
this:
(\<exists>m' Mm. P \<turnstile> y sees_methods Mm \<and> Mm M = \<lfloor>((b, Ts, T, m'), D)\<rfloor>) \<longrightarrow> b' = b \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T

goal (1 subgoal):
 1. \<And>a. map_of ms M = \<lfloor>a\<rfloor> \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>m' Mm. P \<turnstile> y sees_methods Mm \<and> Mm M = \<lfloor>((b, Ts, T, m'), D)\<rfloor>) \<longrightarrow> b' = b \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>m' Mm. P \<turnstile> y sees_methods Mm \<and> Mm M = \<lfloor>((b, Ts, T, m'), D)\<rfloor>) \<longrightarrow> b' = b \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T

goal (1 subgoal):
 1. \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
using Some a sees M x_meth
[PROOF STATE]
proof (prove)
using this:
(\<exists>m' Mm. P \<turnstile> y sees_methods Mm \<and> Mm M = \<lfloor>((b, Ts, T, m'), D)\<rfloor>) \<longrightarrow> b' = b \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
map_of ms M = \<lfloor>a\<rfloor>
a = (b', Ts', T', m')
P \<turnstile> y sees_methods Mm
Mm M = \<lfloor>((b, Ts, T, m), D)\<rfloor>
P \<turnstile> x sees_methods Mm ++ (map_option (\<lambda>m. (m, x)) \<circ> map_of ms)

goal (1 subgoal):
 1. \<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
by(fastforce simp:Method_def map_add_def split:option.split)
[PROOF STATE]
proof (state)
this:
\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<turnstile> y sees M, ?b :  ?Ts\<rightarrow>?T = ?m in ?D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, ?b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> ?Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> ?T

goal (1 subgoal):
 1. \<And>x y. P \<turnstile> x \<prec>\<^sup>1 y \<Longrightarrow> \<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> y sees M, ?b :  ?Ts\<rightarrow>?T = ?m in ?D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, ?b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> ?Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> ?T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> y sees M, ?b :  ?Ts\<rightarrow>?T = ?m in ?D \<Longrightarrow> \<exists>D' Ts' T' m'. P \<turnstile> x sees M, ?b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> ?Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> ?T

goal (1 subgoal):
 1. \<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>D b Ts T m. P \<turnstile> y sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> x sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>D b Ts T m. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D \<longrightarrow> (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sees_method_mono2:
  "\<lbrakk> P \<turnstile> C' \<preceq>\<^sup>* C; wf_prog wf_md P;
     P \<turnstile> C sees M,b:Ts\<rightarrow>T = m in D; P \<turnstile> C' sees M,b':Ts'\<rightarrow>T' = m' in D' \<rbrakk>
  \<Longrightarrow> b = b' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> C' \<preceq>\<^sup>* C; wf_prog wf_md P; P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D; P \<turnstile> C' sees M, b' :  Ts'\<rightarrow>T' = m' in D'\<rbrakk> \<Longrightarrow> b = b' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> C' \<preceq>\<^sup>* C; wf_prog wf_md P; P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D; P \<turnstile> C' sees M, b' :  Ts'\<rightarrow>T' = m' in D'\<rbrakk> \<Longrightarrow> b = b' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
by(blast dest:sees_method_mono sees_method_fun)


[STATEMENT]
lemma mdecls_visible:
assumes wf: "wf_prog wf_md P" and "class": "is_class P C"
shows "\<And>D fs ms. class P C = Some(D,fs,ms)
         \<Longrightarrow> \<exists>Mm. P \<turnstile> C sees_methods Mm \<and> (\<forall>(M,b,Ts,T,m) \<in> set ms. Mm M = Some((b,Ts,T,m),C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>D fs ms. class P C = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> C sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), C)\<rfloor>)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>D fs ms. class P C = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> C sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), C)\<rfloor>)
[PROOF STEP]
using wf "class"
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
is_class P C

goal (1 subgoal):
 1. \<And>D fs ms. class P C = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> C sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), C)\<rfloor>)
[PROOF STEP]
proof (induct rule:subcls1_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>D fs ms. class P Object = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> Object sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), Object)\<rfloor>)
 2. \<And>C D Da fs ms. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; \<And>Da fs ms. class P D = \<lfloor>(Da, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> D sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), D)\<rfloor>); class P C = \<lfloor>(Da, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>Mm. P \<turnstile> C sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), C)\<rfloor>)
[PROOF STEP]
case Object
[PROOF STATE]
proof (state)
this:
class P Object = \<lfloor>(D, fs, ms)\<rfloor>

goal (2 subgoals):
 1. \<And>D fs ms. class P Object = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> Object sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), Object)\<rfloor>)
 2. \<And>C D Da fs ms. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; \<And>Da fs ms. class P D = \<lfloor>(Da, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> D sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), D)\<rfloor>); class P C = \<lfloor>(Da, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>Mm. P \<turnstile> C sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), C)\<rfloor>)
[PROOF STEP]
with wf
[PROOF STATE]
proof (chain)
picking this:
wf_prog wf_md P
class P Object = \<lfloor>(D, fs, ms)\<rfloor>
[PROOF STEP]
have dfst:"distinct_fst ms"
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
class P Object = \<lfloor>(D, fs, ms)\<rfloor>

goal (1 subgoal):
 1. distinct_fst ms
[PROOF STEP]
by (unfold class_def wf_prog_def wf_cdecl_def) (fastforce dest:map_of_SomeD)
[PROOF STATE]
proof (state)
this:
distinct_fst ms

goal (2 subgoals):
 1. \<And>D fs ms. class P Object = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> Object sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), Object)\<rfloor>)
 2. \<And>C D Da fs ms. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; \<And>Da fs ms. class P D = \<lfloor>(Da, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> D sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), D)\<rfloor>); class P C = \<lfloor>(Da, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>Mm. P \<turnstile> C sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), C)\<rfloor>)
[PROOF STEP]
with dfst
[PROOF STATE]
proof (chain)
picking this:
distinct_fst ms
distinct_fst ms
[PROOF STEP]
have "distinct_fst ms"
[PROOF STATE]
proof (prove)
using this:
distinct_fst ms
distinct_fst ms

goal (1 subgoal):
 1. distinct_fst ms
[PROOF STEP]
by(blast dest: distinct_fst_appendD)
[PROOF STATE]
proof (state)
this:
distinct_fst ms

goal (2 subgoals):
 1. \<And>D fs ms. class P Object = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> Object sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), Object)\<rfloor>)
 2. \<And>C D Da fs ms. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; \<And>Da fs ms. class P D = \<lfloor>(Da, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> D sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), D)\<rfloor>); class P C = \<lfloor>(Da, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>Mm. P \<turnstile> C sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), C)\<rfloor>)
[PROOF STEP]
with Object
[PROOF STATE]
proof (chain)
picking this:
class P Object = \<lfloor>(D, fs, ms)\<rfloor>
distinct_fst ms
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
class P Object = \<lfloor>(D, fs, ms)\<rfloor>
distinct_fst ms

goal (1 subgoal):
 1. \<exists>Mm. P \<turnstile> Object sees_methods Mm \<and> (\<forall>a\<in>set ms. case a of (M, b, Ts, T, m) \<Rightarrow> Mm M = \<lfloor>((b, Ts, T, m), Object)\<rfloor>)
[PROOF STEP]
by(fastforce intro!: sees_methods_Object map_of_SomeI)
[PROOF STATE]
proof (state)
this:
\<exists>Mm. P \<turnstile> Object sees_methods Mm \<and> (\<forall>a\<in>set ms. case a of (M, b, Ts, T, m) \<Rightarrow> Mm M = \<lfloor>((b, Ts, T, m), Object)\<rfloor>)

goal (1 subgoal):
 1. \<And>C D Da fs ms. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; \<And>Da fs ms. class P D = \<lfloor>(Da, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> D sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), D)\<rfloor>); class P C = \<lfloor>(Da, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>Mm. P \<turnstile> C sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), C)\<rfloor>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C D Da fs ms. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; \<And>Da fs ms. class P D = \<lfloor>(Da, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> D sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), D)\<rfloor>); class P C = \<lfloor>(Da, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>Mm. P \<turnstile> C sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), C)\<rfloor>)
[PROOF STEP]
case Subcls
[PROOF STATE]
proof (state)
this:
C_ \<noteq> Object
P \<turnstile> C_ \<prec>\<^sup>1 D_
is_class P D_
class P D_ = \<lfloor>(?D, ?fs, ?ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> D_ sees_methods Mm \<and> (\<forall>a\<in>set ?ms. case a of (M, b, Ts, T, m) \<Rightarrow> Mm M = \<lfloor>((b, Ts, T, m), D_)\<rfloor>)
class P C_ = \<lfloor>(D, fs, ms)\<rfloor>

goal (1 subgoal):
 1. \<And>C D Da fs ms. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; \<And>Da fs ms. class P D = \<lfloor>(Da, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> D sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), D)\<rfloor>); class P C = \<lfloor>(Da, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>Mm. P \<turnstile> C sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), C)\<rfloor>)
[PROOF STEP]
with wf
[PROOF STATE]
proof (chain)
picking this:
wf_prog wf_md P
C_ \<noteq> Object
P \<turnstile> C_ \<prec>\<^sup>1 D_
is_class P D_
class P D_ = \<lfloor>(?D, ?fs, ?ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> D_ sees_methods Mm \<and> (\<forall>a\<in>set ?ms. case a of (M, b, Ts, T, m) \<Rightarrow> Mm M = \<lfloor>((b, Ts, T, m), D_)\<rfloor>)
class P C_ = \<lfloor>(D, fs, ms)\<rfloor>
[PROOF STEP]
have dfst:"distinct_fst ms"
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
C_ \<noteq> Object
P \<turnstile> C_ \<prec>\<^sup>1 D_
is_class P D_
class P D_ = \<lfloor>(?D, ?fs, ?ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> D_ sees_methods Mm \<and> (\<forall>a\<in>set ?ms. case a of (M, b, Ts, T, m) \<Rightarrow> Mm M = \<lfloor>((b, Ts, T, m), D_)\<rfloor>)
class P C_ = \<lfloor>(D, fs, ms)\<rfloor>

goal (1 subgoal):
 1. distinct_fst ms
[PROOF STEP]
by (unfold class_def wf_prog_def wf_cdecl_def) (fastforce dest:map_of_SomeD)
[PROOF STATE]
proof (state)
this:
distinct_fst ms

goal (1 subgoal):
 1. \<And>C D Da fs ms. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; \<And>Da fs ms. class P D = \<lfloor>(Da, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> D sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), D)\<rfloor>); class P C = \<lfloor>(Da, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>Mm. P \<turnstile> C sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), C)\<rfloor>)
[PROOF STEP]
with dfst
[PROOF STATE]
proof (chain)
picking this:
distinct_fst ms
distinct_fst ms
[PROOF STEP]
have "distinct_fst ms"
[PROOF STATE]
proof (prove)
using this:
distinct_fst ms
distinct_fst ms

goal (1 subgoal):
 1. distinct_fst ms
[PROOF STEP]
by(blast dest: distinct_fst_appendD)
[PROOF STATE]
proof (state)
this:
distinct_fst ms

goal (1 subgoal):
 1. \<And>C D Da fs ms. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; \<And>Da fs ms. class P D = \<lfloor>(Da, fs, ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> D sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), D)\<rfloor>); class P C = \<lfloor>(Da, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>Mm. P \<turnstile> C sees_methods Mm \<and> (\<forall>(M, b, Ts, T, m)\<in>set ms. Mm M = \<lfloor>((b, Ts, T, m), C)\<rfloor>)
[PROOF STEP]
with Subcls
[PROOF STATE]
proof (chain)
picking this:
C_ \<noteq> Object
P \<turnstile> C_ \<prec>\<^sup>1 D_
is_class P D_
class P D_ = \<lfloor>(?D, ?fs, ?ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> D_ sees_methods Mm \<and> (\<forall>a\<in>set ?ms. case a of (M, b, Ts, T, m) \<Rightarrow> Mm M = \<lfloor>((b, Ts, T, m), D_)\<rfloor>)
class P C_ = \<lfloor>(D, fs, ms)\<rfloor>
distinct_fst ms
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
C_ \<noteq> Object
P \<turnstile> C_ \<prec>\<^sup>1 D_
is_class P D_
class P D_ = \<lfloor>(?D, ?fs, ?ms)\<rfloor> \<Longrightarrow> \<exists>Mm. P \<turnstile> D_ sees_methods Mm \<and> (\<forall>a\<in>set ?ms. case a of (M, b, Ts, T, m) \<Rightarrow> Mm M = \<lfloor>((b, Ts, T, m), D_)\<rfloor>)
class P C_ = \<lfloor>(D, fs, ms)\<rfloor>
distinct_fst ms

goal (1 subgoal):
 1. \<exists>Mm. P \<turnstile> C_ sees_methods Mm \<and> (\<forall>a\<in>set ms. case a of (M, b, Ts, T, m) \<Rightarrow> Mm M = \<lfloor>((b, Ts, T, m), C_)\<rfloor>)
[PROOF STEP]
by(fastforce elim:sees_methods_rec dest:subcls1D map_of_SomeI
                simp:is_class_def)
[PROOF STATE]
proof (state)
this:
\<exists>Mm. P \<turnstile> C_ sees_methods Mm \<and> (\<forall>a\<in>set ms. case a of (M, b, Ts, T, m) \<Rightarrow> Mm M = \<lfloor>((b, Ts, T, m), C_)\<rfloor>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mdecl_visible:
assumes wf: "wf_prog wf_md P" and C: "(C,S,fs,ms) \<in> set P" and  m: "(M,b,Ts,T,m) \<in> set ms"
shows "P \<turnstile> C sees M,b:Ts\<rightarrow>T = m in C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in C
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in C
[PROOF STEP]
from wf C
[PROOF STATE]
proof (chain)
picking this:
wf_prog wf_md P
(C, S, fs, ms) \<in> set P
[PROOF STEP]
have "class": "class P C = Some (S,fs,ms)"
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
(C, S, fs, ms) \<in> set P

goal (1 subgoal):
 1. class P C = \<lfloor>(S, fs, ms)\<rfloor>
[PROOF STEP]
by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
[PROOF STATE]
proof (state)
this:
class P C = \<lfloor>(S, fs, ms)\<rfloor>

goal (1 subgoal):
 1. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in C
[PROOF STEP]
from "class"
[PROOF STATE]
proof (chain)
picking this:
class P C = \<lfloor>(S, fs, ms)\<rfloor>
[PROOF STEP]
have "is_class P C"
[PROOF STATE]
proof (prove)
using this:
class P C = \<lfloor>(S, fs, ms)\<rfloor>

goal (1 subgoal):
 1. is_class P C
[PROOF STEP]
by(auto simp:is_class_def)
[PROOF STATE]
proof (state)
this:
is_class P C

goal (1 subgoal):
 1. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in C
[PROOF STEP]
with assms "class"
[PROOF STATE]
proof (chain)
picking this:
wf_prog wf_md P
(C, S, fs, ms) \<in> set P
(M, b, Ts, T, m) \<in> set ms
class P C = \<lfloor>(S, fs, ms)\<rfloor>
is_class P C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
(C, S, fs, ms) \<in> set P
(M, b, Ts, T, m) \<in> set ms
class P C = \<lfloor>(S, fs, ms)\<rfloor>
is_class P C

goal (1 subgoal):
 1. P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in C
[PROOF STEP]
by(bestsimp simp:Method_def dest:mdecls_visible)
[PROOF STATE]
proof (state)
this:
P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Call_lemma:
assumes sees: "P \<turnstile> C sees M,b:Ts\<rightarrow>T = m in D" and sub: "P \<turnstile> C' \<preceq>\<^sup>* C" and wf: "wf_prog wf_md P"
shows "\<exists>D' Ts' T' m'.
       P \<turnstile> C' sees M,b:Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T \<and> P \<turnstile> C' \<preceq>\<^sup>* D'
       \<and> is_type P T' \<and> (\<forall>T\<in>set Ts'. is_type P T) \<and> wf_md P D' (M,b,Ts',T',m')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T \<and> P \<turnstile> C' \<preceq>\<^sup>* D' \<and> is_type P T' \<and> (\<forall>T\<in>set Ts'. is_type P T) \<and> wf_md P D' (M, b, Ts', T', m')
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T \<and> P \<turnstile> C' \<preceq>\<^sup>* D' \<and> is_type P T' \<and> (\<forall>T\<in>set Ts'. is_type P T) \<and> wf_md P D' (M, b, Ts', T', m')
[PROOF STEP]
using assms sees_method_mono[OF sub wf sees]
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in D
P \<turnstile> C' \<preceq>\<^sup>* C
wf_prog wf_md P
\<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T

goal (1 subgoal):
 1. \<exists>D' Ts' T' m'. P \<turnstile> C' sees M, b :  Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T \<and> P \<turnstile> C' \<preceq>\<^sup>* D' \<and> is_type P T' \<and> (\<forall>T\<in>set Ts'. is_type P T) \<and> wf_md P D' (M, b, Ts', T', m')
[PROOF STEP]
by(fastforce intro:sees_method_decl_above dest:sees_wf_mdecl
             simp: wf_mdecl_def)


[STATEMENT]
lemma wf_prog_lift:
  assumes wf: "wf_prog (\<lambda>P C bd. A P C bd) P"
  and rule:
  "\<And>wf_md C M b Ts C T m bd.
   wf_prog wf_md P \<Longrightarrow>
   P \<turnstile> C sees M,b:Ts\<rightarrow>T = m in C \<Longrightarrow>
   set Ts \<subseteq>  types P \<Longrightarrow>
   bd = (M,b,Ts,T,m) \<Longrightarrow>
   A P C bd \<Longrightarrow>
   B P C bd"
  shows "wf_prog (\<lambda>P C bd. B P C bd) P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog B P
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog B P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_prog B P
[PROOF STEP]
have "\<And>c. c\<in>set P \<Longrightarrow> wf_cdecl A P c \<Longrightarrow> wf_cdecl B P c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>c \<in> set P; wf_cdecl A P c\<rbrakk> \<Longrightarrow> wf_cdecl B P c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>c \<in> set P; wf_cdecl A P c\<rbrakk> \<Longrightarrow> wf_cdecl B P c
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>c \<in> set P; wf_cdecl A P c\<rbrakk> \<Longrightarrow> wf_cdecl B P c
[PROOF STEP]
assume "c\<in>set P" and "wf_cdecl A P c"
[PROOF STATE]
proof (state)
this:
c \<in> set P
wf_cdecl A P c

goal (1 subgoal):
 1. \<And>c. \<lbrakk>c \<in> set P; wf_cdecl A P c\<rbrakk> \<Longrightarrow> wf_cdecl B P c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c \<in> set P
wf_cdecl A P c
[PROOF STEP]
show "wf_cdecl B P c"
[PROOF STATE]
proof (prove)
using this:
c \<in> set P
wf_cdecl A P c

goal (1 subgoal):
 1. wf_cdecl B P c
[PROOF STEP]
using rule[OF wf mdecl_visible[OF wf] is_type_pTs[OF wf]]
[PROOF STATE]
proof (prove)
using this:
c \<in> set P
wf_cdecl A P c
\<lbrakk>(?Ca, ?S2, ?fs2, ?ms2) \<in> set P; (?M, ?b, ?Ts, ?T, ?m) \<in> set ?ms2; (?C1, ?S1, ?fs1, ?ms1) \<in> set P; (?M1, ?b1, ?Ts, ?T1, ?m1) \<in> set ?ms1; ?bd = (?M, ?b, ?Ts, ?T, ?m); A P ?Ca ?bd\<rbrakk> \<Longrightarrow> B P ?Ca ?bd

goal (1 subgoal):
 1. wf_cdecl B P c
[PROOF STEP]
by (auto simp: wf_cdecl_def wf_mdecl_def)
[PROOF STATE]
proof (state)
this:
wf_cdecl B P c

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?c \<in> set P; wf_cdecl A P ?c\<rbrakk> \<Longrightarrow> wf_cdecl B P ?c

goal (1 subgoal):
 1. wf_prog B P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?c \<in> set P; wf_cdecl A P ?c\<rbrakk> \<Longrightarrow> wf_cdecl B P ?c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?c \<in> set P; wf_cdecl A P ?c\<rbrakk> \<Longrightarrow> wf_cdecl B P ?c

goal (1 subgoal):
 1. wf_prog B P
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?c \<in> set P; wf_cdecl A P ?c\<rbrakk> \<Longrightarrow> wf_cdecl B P ?c
wf_prog A P

goal (1 subgoal):
 1. wf_prog B P
[PROOF STEP]
by (clarsimp simp: wf_prog_def)
[PROOF STATE]
proof (state)
this:
wf_prog B P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_sees_clinit:
assumes wf:"wf_prog wf_md P" and ex: "class P C = Some a"
shows "\<exists>m. P \<turnstile> C sees clinit,Static:[] \<rightarrow> Void = m in C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C
[PROOF STEP]
from ex
[PROOF STATE]
proof (chain)
picking this:
class P C = \<lfloor>a\<rfloor>
[PROOF STEP]
obtain D fs ms where "a = (D,fs,ms)"
[PROOF STATE]
proof (prove)
using this:
class P C = \<lfloor>a\<rfloor>

goal (1 subgoal):
 1. (\<And>D fs ms. a = (D, fs, ms) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases a)
[PROOF STATE]
proof (state)
this:
a = (D, fs, ms)

goal (1 subgoal):
 1. \<exists>m. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = (D, fs, ms)
[PROOF STEP]
have sP: "(C, D, fs, ms) \<in> set P"
[PROOF STATE]
proof (prove)
using this:
a = (D, fs, ms)

goal (1 subgoal):
 1. (C, D, fs, ms) \<in> set P
[PROOF STEP]
using ex map_of_SomeD[of P C a]
[PROOF STATE]
proof (prove)
using this:
a = (D, fs, ms)
class P C = \<lfloor>a\<rfloor>
map_of P C = \<lfloor>a\<rfloor> \<Longrightarrow> (C, a) \<in> set P

goal (1 subgoal):
 1. (C, D, fs, ms) \<in> set P
[PROOF STEP]
by(simp add: class_def)
[PROOF STATE]
proof (state)
this:
(C, D, fs, ms) \<in> set P

goal (1 subgoal):
 1. \<exists>m. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(C, D, fs, ms) \<in> set P
[PROOF STEP]
have "wf_clinit ms"
[PROOF STATE]
proof (prove)
using this:
(C, D, fs, ms) \<in> set P

goal (1 subgoal):
 1. wf_clinit ms
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(C, D, fs, ms) \<in> set P
wf_prog wf_md P
class P C = \<lfloor>a\<rfloor>

goal (1 subgoal):
 1. wf_clinit ms
[PROOF STEP]
by(unfold wf_prog_def wf_cdecl_def, auto)
[PROOF STATE]
proof (state)
this:
wf_clinit ms

goal (1 subgoal):
 1. \<exists>m. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_clinit ms
[PROOF STEP]
obtain m where sm: "(clinit, Static, [], Void, m) \<in> set ms"
[PROOF STATE]
proof (prove)
using this:
wf_clinit ms

goal (1 subgoal):
 1. (\<And>m. (clinit, Static, [], Void, m) \<in> set ms \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson wf_clinit_def)
[PROOF STATE]
proof (state)
this:
(clinit, Static, [], Void, m) \<in> set ms

goal (1 subgoal):
 1. \<exists>m. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(clinit, Static, [], Void, m) \<in> set ms
[PROOF STEP]
have "P \<turnstile> C sees clinit,Static:[] \<rightarrow> Void = m in C"
[PROOF STATE]
proof (prove)
using this:
(clinit, Static, [], Void, m) \<in> set ms

goal (1 subgoal):
 1. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C
[PROOF STEP]
using mdecl_visible[OF wf sP sm]
[PROOF STATE]
proof (prove)
using this:
(clinit, Static, [], Void, m) \<in> set ms
P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C

goal (1 subgoal):
 1. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C

goal (1 subgoal):
 1. \<exists>m. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C

goal (1 subgoal):
 1. \<exists>m. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C
[PROOF STEP]
by(rule exI)
[PROOF STATE]
proof (state)
this:
\<exists>m. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_sees_clinit1:
assumes wf:"wf_prog wf_md P" and ex: "class P C = Some a"
and "P \<turnstile> C sees clinit,b:Ts \<rightarrow> T = m in D"
shows "b = Static \<and> Ts = [] \<and> T = Void \<and> D = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b = Static \<and> Ts = [] \<and> T = Void \<and> D = C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b = Static \<and> Ts = [] \<and> T = Void \<and> D = C
[PROOF STEP]
obtain m' where sees: "P \<turnstile> C sees clinit,Static:[] \<rightarrow> Void = m' in C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m'. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m' in C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wf_sees_clinit[OF wf ex]
[PROOF STATE]
proof (prove)
using this:
\<exists>m. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C

goal (1 subgoal):
 1. (\<And>m'. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m' in C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarify
[PROOF STATE]
proof (state)
this:
P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m' in C

goal (1 subgoal):
 1. b = Static \<and> Ts = [] \<and> T = Void \<and> D = C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m' in C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m' in C

goal (1 subgoal):
 1. b = Static \<and> Ts = [] \<and> T = Void \<and> D = C
[PROOF STEP]
using sees wf
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m' in C
P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m' in C
wf_prog wf_md P

goal (1 subgoal):
 1. b = Static \<and> Ts = [] \<and> T = Void \<and> D = C
[PROOF STEP]
by (meson assms(3) sees_method_fun)
[PROOF STATE]
proof (state)
this:
b = Static \<and> Ts = [] \<and> T = Void \<and> D = C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_NonStatic_nclinit:
assumes wf: "wf_prog wf_md P" and meth: "P \<turnstile> C sees M,NonStatic:Ts\<rightarrow>T=(mxs,mxl,ins,xt) in D"
shows "M \<noteq> clinit"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<noteq> clinit
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M \<noteq> clinit
[PROOF STEP]
from sees_method_is_class[OF meth]
[PROOF STATE]
proof (chain)
picking this:
is_class P C
[PROOF STEP]
obtain a where cls: "class P C = Some a"
[PROOF STATE]
proof (prove)
using this:
is_class P C

goal (1 subgoal):
 1. (\<And>a. class P C = \<lfloor>a\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(clarsimp simp: is_class_def)
[PROOF STATE]
proof (state)
this:
class P C = \<lfloor>a\<rfloor>

goal (1 subgoal):
 1. M \<noteq> clinit
[PROOF STEP]
with wf wf_sees_clinit[OF wf cls]
[PROOF STATE]
proof (chain)
picking this:
wf_prog wf_md P
\<exists>m. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C
class P C = \<lfloor>a\<rfloor>
[PROOF STEP]
obtain m where "P \<turnstile> C sees clinit,Static:[]\<rightarrow>Void=m in C"
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
\<exists>m. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C
class P C = \<lfloor>a\<rfloor>

goal (1 subgoal):
 1. (\<And>m. P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C

goal (1 subgoal):
 1. M \<noteq> clinit
[PROOF STEP]
with meth
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> C sees M, NonStatic :  Ts\<rightarrow>T = (mxs, mxl, ins, xt) in D
P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C sees M, NonStatic :  Ts\<rightarrow>T = (mxs, mxl, ins, xt) in D
P \<turnstile> C sees clinit, Static :  []\<rightarrow>Void = m in C

goal (1 subgoal):
 1. M \<noteq> clinit
[PROOF STEP]
by(auto dest: sees_method_fun)
[PROOF STATE]
proof (state)
this:
M \<noteq> clinit

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_Fields_Ex:
assumes wf: "wf_prog wf_md P" and "is_class P C"
shows "\<exists>FDTs. P \<turnstile> C has_fields FDTs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>FDTs. P \<turnstile> C has_fields FDTs
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>FDTs. P \<turnstile> C has_fields FDTs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
is_class P C

goal (1 subgoal):
 1. \<exists>FDTs. P \<turnstile> C has_fields FDTs
[PROOF STEP]
proof(induct rule:subcls1_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>FDTs. P \<turnstile> Object has_fields FDTs
 2. \<And>C D. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; \<exists>FDTs. P \<turnstile> D has_fields FDTs\<rbrakk> \<Longrightarrow> \<exists>FDTs. P \<turnstile> C has_fields FDTs
[PROOF STEP]
case Object
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<exists>FDTs. P \<turnstile> Object has_fields FDTs
 2. \<And>C D. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; \<exists>FDTs. P \<turnstile> D has_fields FDTs\<rbrakk> \<Longrightarrow> \<exists>FDTs. P \<turnstile> C has_fields FDTs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>FDTs. P \<turnstile> Object has_fields FDTs
[PROOF STEP]
using class_Object[OF wf]
[PROOF STATE]
proof (prove)
using this:
\<exists>C fs ms. class P Object = \<lfloor>(C, fs, ms)\<rfloor>

goal (1 subgoal):
 1. \<exists>FDTs. P \<turnstile> Object has_fields FDTs
[PROOF STEP]
by(blast intro:has_fields_Object)
[PROOF STATE]
proof (state)
this:
\<exists>FDTs. P \<turnstile> Object has_fields FDTs

goal (1 subgoal):
 1. \<And>C D. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; \<exists>FDTs. P \<turnstile> D has_fields FDTs\<rbrakk> \<Longrightarrow> \<exists>FDTs. P \<turnstile> C has_fields FDTs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C D. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; \<exists>FDTs. P \<turnstile> D has_fields FDTs\<rbrakk> \<Longrightarrow> \<exists>FDTs. P \<turnstile> C has_fields FDTs
[PROOF STEP]
case Subcls
[PROOF STATE]
proof (state)
this:
C_ \<noteq> Object
P \<turnstile> C_ \<prec>\<^sup>1 D_
is_class P D_
\<exists>FDTs. P \<turnstile> D_ has_fields FDTs

goal (1 subgoal):
 1. \<And>C D. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; \<exists>FDTs. P \<turnstile> D has_fields FDTs\<rbrakk> \<Longrightarrow> \<exists>FDTs. P \<turnstile> C has_fields FDTs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C_ \<noteq> Object
P \<turnstile> C_ \<prec>\<^sup>1 D_
is_class P D_
\<exists>FDTs. P \<turnstile> D_ has_fields FDTs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
C_ \<noteq> Object
P \<turnstile> C_ \<prec>\<^sup>1 D_
is_class P D_
\<exists>FDTs. P \<turnstile> D_ has_fields FDTs

goal (1 subgoal):
 1. \<exists>FDTs. P \<turnstile> C_ has_fields FDTs
[PROOF STEP]
by(blast intro:has_fields_rec dest:subcls1D)
[PROOF STATE]
proof (state)
this:
\<exists>FDTs. P \<turnstile> C_ has_fields FDTs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_fields_types:
  "\<lbrakk> P \<turnstile> C has_fields FDTs; (FD,b,T) \<in> set FDTs; wf_prog wf_md P \<rbrakk> \<Longrightarrow> is_type P T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> C has_fields FDTs; (FD, b, T) \<in> set FDTs; wf_prog wf_md P\<rbrakk> \<Longrightarrow> is_type P T
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> C has_fields FDTs; (FD, b, T) \<in> set FDTs; wf_prog wf_md P\<rbrakk> \<Longrightarrow> is_type P T
[PROOF STEP]
proof(induct rule:Fields.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C D fs ms FDTs FDTs'. \<lbrakk>class P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; P \<turnstile> D has_fields FDTs; \<lbrakk>(FD, b, T) \<in> set FDTs; wf_prog wf_md P\<rbrakk> \<Longrightarrow> is_type P T; FDTs' = map (\<lambda>(F, b, T). ((F, C), b, T)) fs @ FDTs; (FD, b, T) \<in> set FDTs'; wf_prog wf_md P\<rbrakk> \<Longrightarrow> is_type P T
 2. \<And>D fs ms FDTs. \<lbrakk>class P Object = \<lfloor>(D, fs, ms)\<rfloor>; FDTs = map (\<lambda>(F, b, T). ((F, Object), b, T)) fs; (FD, b, T) \<in> set FDTs; wf_prog wf_md P\<rbrakk> \<Longrightarrow> is_type P T
[PROOF STEP]
qed(fastforce dest!: class_wf simp: wf_cdecl_def wf_fdecl_def)+


[STATEMENT]
lemma sees_field_is_type:
  "\<lbrakk> P \<turnstile> C sees F,b:T in D; wf_prog wf_md P \<rbrakk> \<Longrightarrow> is_type P T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> C sees F,b:T in D; wf_prog wf_md P\<rbrakk> \<Longrightarrow> is_type P T
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> C sees F,b:T in D; wf_prog wf_md P\<rbrakk> \<Longrightarrow> is_type P T
[PROOF STEP]
by (meson has_field_def has_fields_types has_visible_field map_of_SomeD)


[STATEMENT]
lemma wf_syscls:
  "set SystemClasses \<subseteq> set P \<Longrightarrow> wf_syscls P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set SystemClasses \<subseteq> set P \<Longrightarrow> wf_syscls P
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set SystemClasses \<subseteq> set P \<Longrightarrow> wf_syscls P
[PROOF STEP]
by (force simp: image_def SystemClasses_def wf_syscls_def sys_xcpts_def
                ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def
                NoClassDefFoundC_def
                IncompatibleClassChangeC_def NoSuchFieldC_def NoSuchMethodC_def)


[STATEMENT]
lemma wf_subcls_nCls:
assumes wf: "wf_prog wf_md P" and ns: "\<not> is_class P C"
shows "\<lbrakk> P \<turnstile> D \<preceq>\<^sup>* D'; D \<noteq> C \<rbrakk> \<Longrightarrow> D' \<noteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> D \<preceq>\<^sup>* D'; D \<noteq> C\<rbrakk> \<Longrightarrow> D' \<noteq> C
[PROOF STEP]
proof(induct rule: rtrancl.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. a \<noteq> C \<Longrightarrow> a \<noteq> C
 2. \<And>a b c. \<lbrakk>P \<turnstile> a \<preceq>\<^sup>* b; a \<noteq> C \<Longrightarrow> b \<noteq> C; P \<turnstile> b \<prec>\<^sup>1 c; a \<noteq> C\<rbrakk> \<Longrightarrow> c \<noteq> C
[PROOF STEP]
case (rtrancl_into_rtrancl a b c)
[PROOF STATE]
proof (state)
this:
P \<turnstile> a \<preceq>\<^sup>* b
a \<noteq> C \<Longrightarrow> b \<noteq> C
P \<turnstile> b \<prec>\<^sup>1 c
a \<noteq> C

goal (2 subgoals):
 1. \<And>a. a \<noteq> C \<Longrightarrow> a \<noteq> C
 2. \<And>a b c. \<lbrakk>P \<turnstile> a \<preceq>\<^sup>* b; a \<noteq> C \<Longrightarrow> b \<noteq> C; P \<turnstile> b \<prec>\<^sup>1 c; a \<noteq> C\<rbrakk> \<Longrightarrow> c \<noteq> C
[PROOF STEP]
with ns
[PROOF STATE]
proof (chain)
picking this:
\<not> is_class P C
P \<turnstile> a \<preceq>\<^sup>* b
a \<noteq> C \<Longrightarrow> b \<noteq> C
P \<turnstile> b \<prec>\<^sup>1 c
a \<noteq> C
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<not> is_class P C
P \<turnstile> a \<preceq>\<^sup>* b
a \<noteq> C \<Longrightarrow> b \<noteq> C
P \<turnstile> b \<prec>\<^sup>1 c
a \<noteq> C

goal (1 subgoal):
 1. c \<noteq> C
[PROOF STEP]
by(clarsimp dest!: subcls1D wf_cdecl_supD[OF class_wf[OF _ wf]])
[PROOF STATE]
proof (state)
this:
c \<noteq> C

goal (1 subgoal):
 1. \<And>a. a \<noteq> C \<Longrightarrow> a \<noteq> C
[PROOF STEP]
qed(simp)


[STATEMENT]
lemma wf_subcls_nCls':
assumes wf: "wf_prog wf_md P" and ns: "\<not>is_class P C\<^sub>0"
shows "\<And>cd D'. cd \<in> set P \<Longrightarrow> \<not>P \<turnstile> fst cd \<preceq>\<^sup>* C\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cd D'. cd \<in> set P \<Longrightarrow> (fst cd, C\<^sub>0) \<notin> (subcls1 P)\<^sup>*
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cd D'. cd \<in> set P \<Longrightarrow> (fst cd, C\<^sub>0) \<notin> (subcls1 P)\<^sup>*
[PROOF STEP]
fix cd D'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cd D'. cd \<in> set P \<Longrightarrow> (fst cd, C\<^sub>0) \<notin> (subcls1 P)\<^sup>*
[PROOF STEP]
assume cd: "cd \<in> set P"
[PROOF STATE]
proof (state)
this:
cd \<in> set P

goal (1 subgoal):
 1. \<And>cd D'. cd \<in> set P \<Longrightarrow> (fst cd, C\<^sub>0) \<notin> (subcls1 P)\<^sup>*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cd \<in> set P
[PROOF STEP]
have cls: "is_class P (fst cd)"
[PROOF STATE]
proof (prove)
using this:
cd \<in> set P

goal (1 subgoal):
 1. is_class P (fst cd)
[PROOF STEP]
using class_exists_equiv is_class_def
[PROOF STATE]
proof (prove)
using this:
cd \<in> set P
(\<exists>x. fst x = ?cn \<and> x \<in> set ?P) = (class ?P ?cn \<noteq> None)
is_class ?P ?C \<equiv> class ?P ?C \<noteq> None

goal (1 subgoal):
 1. is_class P (fst cd)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_class P (fst cd)

goal (1 subgoal):
 1. \<And>cd D'. cd \<in> set P \<Longrightarrow> (fst cd, C\<^sub>0) \<notin> (subcls1 P)\<^sup>*
[PROOF STEP]
with wf_subcls_nCls[OF wf ns] ns
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>P \<turnstile> ?D \<preceq>\<^sup>* ?D'; ?D \<noteq> C\<^sub>0\<rbrakk> \<Longrightarrow> ?D' \<noteq> C\<^sub>0
\<not> is_class P C\<^sub>0
is_class P (fst cd)
[PROOF STEP]
show "\<not>P \<turnstile> fst cd \<preceq>\<^sup>* C\<^sub>0"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P \<turnstile> ?D \<preceq>\<^sup>* ?D'; ?D \<noteq> C\<^sub>0\<rbrakk> \<Longrightarrow> ?D' \<noteq> C\<^sub>0
\<not> is_class P C\<^sub>0
is_class P (fst cd)

goal (1 subgoal):
 1. (fst cd, C\<^sub>0) \<notin> (subcls1 P)\<^sup>*
[PROOF STEP]
by(cases "fst cd = D'", auto)
[PROOF STATE]
proof (state)
this:
(fst cd, C\<^sub>0) \<notin> (subcls1 P)\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_nclass_nsub:
 "\<lbrakk> wf_prog wf_md P; is_class P C; \<not>is_class P C' \<rbrakk> \<Longrightarrow> \<not>P \<turnstile> C \<preceq>\<^sup>* C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; is_class P C; \<not> is_class P C'\<rbrakk> \<Longrightarrow> (C, C') \<notin> (subcls1 P)\<^sup>*
[PROOF STEP]
by(rule notI, auto dest: wf_subcls_nCls[where C=C' and D=C])


[STATEMENT]
lemma wf_sys_xcpt_nsub_Start:
assumes wf: "wf_prog wf_md P" and ns: "\<not>is_class P Start" and sx: "C \<in> sys_xcpts"
shows "\<not>P \<turnstile> C \<preceq>\<^sup>* Start"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C, Start) \<notin> (subcls1 P)\<^sup>*
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (C, Start) \<notin> (subcls1 P)\<^sup>*
[PROOF STEP]
have Cns: "C \<noteq> Start"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<noteq> Start
[PROOF STEP]
using Start_nsys_xcpts sx
[PROOF STATE]
proof (prove)
using this:
Start \<notin> sys_xcpts
C \<in> sys_xcpts

goal (1 subgoal):
 1. C \<noteq> Start
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
C \<noteq> Start

goal (1 subgoal):
 1. (C, Start) \<notin> (subcls1 P)\<^sup>*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C, Start) \<notin> (subcls1 P)\<^sup>*
[PROOF STEP]
using wf_subcls_nCls[OF wf ns _ Cns]
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C \<preceq>\<^sup>* ?D' \<Longrightarrow> ?D' \<noteq> Start

goal (1 subgoal):
 1. (C, Start) \<notin> (subcls1 P)\<^sup>*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(C, Start) \<notin> (subcls1 P)\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma if_then_Some_else_None_eq[simp]:
  "(if a then Some b else None) = Some c \<longleftrightarrow> a \<and> b = c"
  "(if a then Some b else None) = None \<longleftrightarrow> \<not> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if a then Some b else None) = Some c) = (a \<and> b = c) &&& ((if a then Some b else None) = None) = (\<not> a)
[PROOF STEP]
by (cases a) simp_all


[STATEMENT]
lemma if_then_else_distributive: "(if a then f b else f c) = f (if a then b else c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if a then f b else f c) = f (if a then b else c)
[PROOF STEP]
by simp


[STATEMENT]
lemma map_ofD:
  fixes xs k opt
  assumes "map_of xs k = opt"
  shows "opt = None \<or> (\<exists>n < length xs. opt = Some (snd (xs ! n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. opt = None \<or> (\<exists>n<length xs. opt = Some (snd (xs ! n)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
map_of xs k = opt

goal (1 subgoal):
 1. opt = None \<or> (\<exists>n<length xs. opt = Some (snd (xs ! n)))
[PROOF STEP]
by (metis in_set_conv_nth map_of_SomeD not_Some_eq snd_conv)


[STATEMENT]
lemma list_all2_assoc_map_rel_get:
  assumes "list_all2 (=) (map fst xs) (map fst ys)" and "list_all2 R (map snd xs) (map snd ys)"
  shows "rel_option R (map_of xs k) (map_of ys k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option R (map_of xs k) (map_of ys k)
[PROOF STEP]
using assms[unfolded list.rel_map]
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>x y. fst x = fst y) xs ys
list_all2 (\<lambda>x y. R (snd x) (snd y)) xs ys

goal (1 subgoal):
 1. rel_option R (map_of xs k) (map_of ys k)
[PROOF STEP]
proof (induction xs ys rule: list.rel_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. list_all2 (\<lambda>x y. R (snd x) (snd y)) [] [] \<Longrightarrow> rel_option R (map_of [] k) (map_of [] k)
 2. \<And>a21 a22 b21 b22. \<lbrakk>fst a21 = fst b21; list_all2 (\<lambda>x y. R (snd x) (snd y)) a22 b22 \<Longrightarrow> rel_option R (map_of a22 k) (map_of b22 k); list_all2 (\<lambda>x y. R (snd x) (snd y)) (a21 # a22) (b21 # b22)\<rbrakk> \<Longrightarrow> rel_option R (map_of (a21 # a22) k) (map_of (b21 # b22) k)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
list_all2 (\<lambda>x y. R (snd x) (snd y)) [] []

goal (2 subgoals):
 1. list_all2 (\<lambda>x y. R (snd x) (snd y)) [] [] \<Longrightarrow> rel_option R (map_of [] k) (map_of [] k)
 2. \<And>a21 a22 b21 b22. \<lbrakk>fst a21 = fst b21; list_all2 (\<lambda>x y. R (snd x) (snd y)) a22 b22 \<Longrightarrow> rel_option R (map_of a22 k) (map_of b22 k); list_all2 (\<lambda>x y. R (snd x) (snd y)) (a21 # a22) (b21 # b22)\<rbrakk> \<Longrightarrow> rel_option R (map_of (a21 # a22) k) (map_of (b21 # b22) k)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>x y. R (snd x) (snd y)) [] []

goal (1 subgoal):
 1. rel_option R (map_of [] k) (map_of [] k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rel_option R (map_of [] k) (map_of [] k)

goal (1 subgoal):
 1. \<And>a21 a22 b21 b22. \<lbrakk>fst a21 = fst b21; list_all2 (\<lambda>x y. R (snd x) (snd y)) a22 b22 \<Longrightarrow> rel_option R (map_of a22 k) (map_of b22 k); list_all2 (\<lambda>x y. R (snd x) (snd y)) (a21 # a22) (b21 # b22)\<rbrakk> \<Longrightarrow> rel_option R (map_of (a21 # a22) k) (map_of (b21 # b22) k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a21 a22 b21 b22. \<lbrakk>fst a21 = fst b21; list_all2 (\<lambda>x y. R (snd x) (snd y)) a22 b22 \<Longrightarrow> rel_option R (map_of a22 k) (map_of b22 k); list_all2 (\<lambda>x y. R (snd x) (snd y)) (a21 # a22) (b21 # b22)\<rbrakk> \<Longrightarrow> rel_option R (map_of (a21 # a22) k) (map_of (b21 # b22) k)
[PROOF STEP]
case (Cons x xs y ys)
[PROOF STATE]
proof (state)
this:
fst x = fst y
list_all2 (\<lambda>x y. R (snd x) (snd y)) xs ys \<Longrightarrow> rel_option R (map_of xs k) (map_of ys k)
list_all2 (\<lambda>x y. R (snd x) (snd y)) (x # xs) (y # ys)

goal (1 subgoal):
 1. \<And>a21 a22 b21 b22. \<lbrakk>fst a21 = fst b21; list_all2 (\<lambda>x y. R (snd x) (snd y)) a22 b22 \<Longrightarrow> rel_option R (map_of a22 k) (map_of b22 k); list_all2 (\<lambda>x y. R (snd x) (snd y)) (a21 # a22) (b21 # b22)\<rbrakk> \<Longrightarrow> rel_option R (map_of (a21 # a22) k) (map_of (b21 # b22) k)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
fst x = fst y
list_all2 (\<lambda>x y. R (snd x) (snd y)) xs ys \<Longrightarrow> rel_option R (map_of xs k) (map_of ys k)
list_all2 (\<lambda>x y. R (snd x) (snd y)) (x # xs) (y # ys)

goal (1 subgoal):
 1. rel_option R (map_of (x # xs) k) (map_of (y # ys) k)
[PROOF STEP]
by (cases "k = fst x") auto
[PROOF STATE]
proof (state)
this:
rel_option R (map_of (x # xs) k) (map_of (y # ys) k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_fundef_arities: "rel_fundef r1 r2 gd1 gd2 \<Longrightarrow> arity gd1 = arity gd2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fundef r1 r2 gd1 gd2 \<Longrightarrow> arity gd1 = arity gd2
[PROOF STEP]
by (simp add: fundef.rel_sel)


[STATEMENT]
lemma rel_fundef_return: "rel_fundef R1 R2 gd1 gd2 \<Longrightarrow> return gd1 = return gd2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fundef R1 R2 gd1 gd2 \<Longrightarrow> return gd1 = return gd2
[PROOF STEP]
by (simp add: fundef.rel_sel)


[STATEMENT]
lemma rel_fundef_locals: "rel_fundef R1 R2 gd1 gd2 \<Longrightarrow> fundef_locals gd1 = fundef_locals gd2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fundef R1 R2 gd1 gd2 \<Longrightarrow> fundef_locals gd1 = fundef_locals gd2
[PROOF STEP]
by (simp add: fundef.rel_sel)


[STATEMENT]
lemma rel_fundef_body_length[simp]:
  "rel_fundef r1 r2 fd1 fd2 \<Longrightarrow> length (body fd1) = length (body fd2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fundef r1 r2 fd1 fd2 \<Longrightarrow> length (body fd1) = length (body fd2)
[PROOF STEP]
by (auto intro: list_all2_lengthD simp add: fundef.rel_sel)


[STATEMENT]
lemma rel_fundef_funtype[simp]: "rel_fundef R1 R2 fd1 fd2 \<Longrightarrow> funtype fd1 = funtype fd2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fundef R1 R2 fd1 fd2 \<Longrightarrow> funtype fd1 = funtype fd2
[PROOF STEP]
by (simp add: fundef.rel_sel funtype_def)


[STATEMENT]
lemma rel_fundef_rel_fst_hd_bodies:
  assumes "rel_fundef R1 R2 fd1 fd2" and "body fd1 \<noteq> [] \<or> body fd2 \<noteq> []"
  shows "R1 (fst (hd (body fd1))) (fst (hd (body fd2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R1 (fst (hd (body fd1))) (fst (hd (body fd2)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rel_fundef R1 R2 fd1 fd2
body fd1 \<noteq> [] \<or> body fd2 \<noteq> []

goal (1 subgoal):
 1. R1 (fst (hd (body fd1))) (fst (hd (body fd2)))
[PROOF STEP]
unfolding fundef.rel_sel
[PROOF STATE]
proof (prove)
using this:
list_all2 (rel_prod R1 (list_all2 R2)) (body fd1) (body fd2) \<and> arity fd1 = arity fd2 \<and> return fd1 = return fd2 \<and> fundef_locals fd1 = fundef_locals fd2
body fd1 \<noteq> [] \<or> body fd2 \<noteq> []

goal (1 subgoal):
 1. R1 (fst (hd (body fd1))) (fst (hd (body fd2)))
[PROOF STEP]
by (auto intro: list_all2_rel_prod_fst_hd[THEN conjunct1])


[STATEMENT]
lemma map_option_comp_conv:
  assumes
    "\<And>x. rel_option R (f x) (g x)"
    "\<And>fd1 fd2. fd1 \<in> ran f \<Longrightarrow> fd2 \<in> ran g \<Longrightarrow> R fd1 fd2 \<Longrightarrow> h fd1 = i fd2"
  shows "map_option h \<circ> f = map_option i \<circ> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_option h \<circ> f = map_option i \<circ> g
[PROOF STEP]
proof (intro ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (map_option h \<circ> f) x = (map_option i \<circ> g) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (map_option h \<circ> f) x = (map_option i \<circ> g) x
[PROOF STEP]
show "(map_option h \<circ> f) x = (map_option i \<circ> g) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map_option h \<circ> f) x = (map_option i \<circ> g) x
[PROOF STEP]
using assms(1)[of x]
[PROOF STATE]
proof (prove)
using this:
rel_option R (f x) (g x)

goal (1 subgoal):
 1. (map_option h \<circ> f) x = (map_option i \<circ> g) x
[PROOF STEP]
by (cases rule: option.rel_cases) (auto intro: ranI assms(2))
[PROOF STATE]
proof (state)
this:
(map_option h \<circ> f) x = (map_option i \<circ> g) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_option_arity_comp_conv:
  assumes "(\<And>x. rel_option (rel_fundef R S) (f x) (g x))"
  shows "map_option arity \<circ> f = map_option arity \<circ> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_option arity \<circ> f = map_option arity \<circ> g
[PROOF STEP]
proof (rule map_option_comp_conv)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. rel_option ?R (f x) (g x)
 2. \<And>fd1 fd2. \<lbrakk>fd1 \<in> ran f; fd2 \<in> ran g; ?R fd1 fd2\<rbrakk> \<Longrightarrow> arity fd1 = arity fd2
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. rel_option ?R (f x) (g x)
 2. \<And>fd1 fd2. \<lbrakk>fd1 \<in> ran f; fd2 \<in> ran g; ?R fd1 fd2\<rbrakk> \<Longrightarrow> arity fd1 = arity fd2
[PROOF STEP]
show "rel_option (rel_fundef R S) (f x) (g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option (rel_fundef R S) (f x) (g x)
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
this:
rel_option (rel_fundef R S) (f x) (g x)

goal (1 subgoal):
 1. \<And>fd1 fd2. \<lbrakk>fd1 \<in> ran f; fd2 \<in> ran g; rel_fundef R S fd1 fd2\<rbrakk> \<Longrightarrow> arity fd1 = arity fd2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fd1 fd2. \<lbrakk>fd1 \<in> ran f; fd2 \<in> ran g; rel_fundef R S fd1 fd2\<rbrakk> \<Longrightarrow> arity fd1 = arity fd2
[PROOF STEP]
fix fd1 fd2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fd1 fd2. \<lbrakk>fd1 \<in> ran f; fd2 \<in> ran g; rel_fundef R S fd1 fd2\<rbrakk> \<Longrightarrow> arity fd1 = arity fd2
[PROOF STEP]
show "rel_fundef R S fd1 fd2 \<Longrightarrow> arity fd1 = arity fd2 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fundef R S fd1 fd2 \<Longrightarrow> arity fd1 = arity fd2
[PROOF STEP]
by (rule rel_fundef_arities)
[PROOF STATE]
proof (state)
this:
rel_fundef R S fd1 fd2 \<Longrightarrow> arity fd1 = arity fd2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_fundef_non_empty_bodyD[dest,intro]: "wf_fundef fd \<Longrightarrow> body fd \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fundef fd \<Longrightarrow> body fd \<noteq> []
[PROOF STEP]
by (simp add: wf_fundef_def)


[STATEMENT]
lemma wf_fundefsI:
  assumes "\<And>f fd. F f = Some fd \<Longrightarrow> wf_fundef fd"
  shows "wf_fundefs F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fundefs F
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
F ?f = Some ?fd \<Longrightarrow> wf_fundef ?fd

goal (1 subgoal):
 1. wf_fundefs F
[PROOF STEP]
by (simp add: wf_fundefs_def)


[STATEMENT]
lemma wf_fundefsI':
  assumes "\<And>f. pred_option wf_fundef (F f)"
  shows "wf_fundefs F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fundefs F
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
pred_option wf_fundef (F ?f)

goal (1 subgoal):
 1. wf_fundefs F
[PROOF STEP]
unfolding wf_fundefs_def
[PROOF STATE]
proof (prove)
using this:
pred_option wf_fundef (F ?f)

goal (1 subgoal):
 1. \<forall>f fd. F f = Some fd \<longrightarrow> wf_fundef fd
[PROOF STEP]
by (metis option.pred_inject(2))


[STATEMENT]
lemma wf_fundefs_imp_wf_fundef:
  assumes "wf_fundefs F" and "F f = Some fd"
  shows "wf_fundef fd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fundef fd
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_fundefs F
F f = Some fd

goal (1 subgoal):
 1. wf_fundef fd
[PROOF STEP]
by (simp add: wf_fundefs_def)


[STATEMENT]
lemma instr_atD:
  assumes "instr_at fd l pc = Some instr"
  shows "\<exists>instrs. map_of (body fd) l = Some instrs \<and> pc < length instrs \<and> instrs ! pc = instr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>instrs. map_of (body fd) l = Some instrs \<and> pc < length instrs \<and> instrs ! pc = instr
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
instr_at fd l pc = Some instr

goal (1 subgoal):
 1. \<exists>instrs. map_of (body fd) l = Some instrs \<and> pc < length instrs \<and> instrs ! pc = instr
[PROOF STEP]
by (cases "map_of (body fd) l") (auto simp: instr_at_def)


[STATEMENT]
lemma rel_fundef_imp_rel_option_instr_at:
  assumes "rel_fundef (=) R fd1 fd2"
  shows "rel_option R (instr_at fd1 l pc) (instr_at fd2 l pc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option R (instr_at fd1 l pc) (instr_at fd2 l pc)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rel_fundef (=) R fd1 fd2

goal (1 subgoal):
 1. rel_option R (instr_at fd1 l pc) (instr_at fd2 l pc)
[PROOF STEP]
proof (cases rule: fundef.rel_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_option R (instr_at fd1 l pc) (instr_at fd2 l pc)
[PROOF STEP]
case (Fundef bblocks1 _ _ bblocks2 )
[PROOF STATE]
proof (state)
this:
fd1 = Fundef bblocks1 x2a_ x3a_ bblocks2
fd2 = Fundef y1a_ y2a_ y3a_ y4a_
list_all2 (rel_prod (=) (list_all2 R)) bblocks1 y1a_
x2a_ = y2a_
x3a_ = y3a_
bblocks2 = y4a_

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_option R (instr_at fd1 l pc) (instr_at fd2 l pc)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fd1 = Fundef bblocks1 x2a_ x3a_ bblocks2
fd2 = Fundef y1a_ y2a_ y3a_ y4a_
list_all2 (rel_prod (=) (list_all2 R)) bblocks1 y1a_
x2a_ = y2a_
x3a_ = y3a_
bblocks2 = y4a_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fd1 = Fundef bblocks1 x2a_ x3a_ bblocks2
fd2 = Fundef y1a_ y2a_ y3a_ y4a_
list_all2 (rel_prod (=) (list_all2 R)) bblocks1 y1a_
x2a_ = y2a_
x3a_ = y3a_
bblocks2 = y4a_

goal (1 subgoal):
 1. rel_option R (instr_at fd1 l pc) (instr_at fd2 l pc)
[PROOF STEP]
by (auto simp: instr_at_def list_all2_lengthD
        intro: list_all2_nthD2 elim!: option.rel_cases dest!: rel_option_map_of[of _ _ _ l])
[PROOF STATE]
proof (state)
this:
rel_option R (instr_at fd1 l pc) (instr_at fd2 l pc)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma next_instr_eq_Some_conv:
  "next_instr F f l pc = Some instr \<longleftrightarrow> (\<exists>fd. F f = Some fd \<and> instr_at fd l pc = Some instr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (next_instr F f l pc = Some instr) = (\<exists>fd. F f = Some fd \<and> instr_at fd l pc = Some instr)
[PROOF STEP]
by (simp add: next_instr_def bind_eq_Some_conv)


[STATEMENT]
lemma next_instrD:
  assumes "next_instr F f l pc = Some instr"
  shows "\<exists>fd. F f = Some fd \<and> instr_at fd l pc = Some instr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>fd. F f = Some fd \<and> instr_at fd l pc = Some instr
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
next_instr F f l pc = Some instr

goal (1 subgoal):
 1. \<exists>fd. F f = Some fd \<and> instr_at fd l pc = Some instr
[PROOF STEP]
unfolding next_instr_def
[PROOF STATE]
proof (prove)
using this:
F f \<bind> (\<lambda>fd. instr_at fd l pc) = Some instr

goal (1 subgoal):
 1. \<exists>fd. F f = Some fd \<and> instr_at fd l pc = Some instr
[PROOF STEP]
by (cases "F f"; simp)


[STATEMENT]
lemma next_instr_pc_lt_length_instrsI:
  assumes
    "next_instr F f l pc = Some instr" and
    "F f = Some fd" and
    "map_of (body fd) l = Some instrs"
  shows "pc < length instrs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length instrs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
next_instr F f l pc = Some instr
F f = Some fd
map_of (body fd) l = Some instrs

goal (1 subgoal):
 1. pc < length instrs
[PROOF STEP]
by (auto dest!: next_instrD instr_atD)


[STATEMENT]
lemma next_instr_get_map_ofD:
  assumes
    "next_instr F f l pc = Some instr" and
    "F f = Some fd" and
    "map_of (body fd) l = Some instrs"
  shows "pc < length instrs" and "instrs ! pc = instr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length instrs &&& instrs ! pc = instr
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
next_instr F f l pc = Some instr
F f = Some fd
map_of (body fd) l = Some instrs

goal (1 subgoal):
 1. pc < length instrs &&& instrs ! pc = instr
[PROOF STEP]
by (auto dest!: next_instrD instr_atD)


[STATEMENT]
lemma next_instr_length_instrs:
  assumes
    "F f = Some fd" and
    "map_of (body fd) label = Some instrs"
  shows "next_instr F f label (length instrs) = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_instr F f label (length instrs) = None
[PROOF STEP]
by (simp add: assms next_instr_def instr_at_def)


[STATEMENT]
lemma next_instr_take_Suc_conv:
  assumes "next_instr F f l pc = Some instr" and
    "F f = Some fd" and
    "map_of (body fd) l = Some instrs"
  shows "take (Suc pc) instrs = take pc instrs @ [instr]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (Suc pc) instrs = take pc instrs @ [instr]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
next_instr F f l pc = Some instr
F f = Some fd
map_of (body fd) l = Some instrs

goal (1 subgoal):
 1. take (Suc pc) instrs = take pc instrs @ [instr]
[PROOF STEP]
by (auto simp: take_Suc_conv_app_nth dest!: next_instrD instr_atD)