[STATEMENT]
lemma iter_narrow_termination:
assumes P_f: "\<And>c. P c \<Longrightarrow> P(c \<triangle>\<^sub>c f c)"
and wf: "wf({(c, c \<triangle>\<^sub>c f c)|c c'. P c \<and> ~ c \<sqsubseteq> c \<triangle>\<^sub>c f c}^-1)"
and "P c0" shows "\<exists>c. iter_narrow f c0 = Some c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. iter_narrow f c0 = Some c
[PROOF STEP]
proof(simp add: iter_narrow_def, rule wf_while_option_Some[where P = "P"])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. wf {(c, s). (P s \<and> \<not> s \<sqsubseteq> s \<triangle>\<^sub>c f s) \<and> c = s \<triangle>\<^sub>c f s}
 2. \<And>s. \<lbrakk>P s; \<not> s \<sqsubseteq> s \<triangle>\<^sub>c f s\<rbrakk> \<Longrightarrow> P (s \<triangle>\<^sub>c f s)
 3. P c0
[PROOF STEP]
show "wf {(c', c). (P c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c f c) \<and> c' = c \<triangle>\<^sub>c f c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(c', c). (P c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c f c) \<and> c' = c \<triangle>\<^sub>c f c}
[PROOF STEP]
apply(rule wf_subset[OF wf])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(c', c). (P c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c f c) \<and> c' = c \<triangle>\<^sub>c f c} \<subseteq> {uu_. \<exists>c c'. uu_ = (c, c \<triangle>\<^sub>c f c) \<and> P c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c f c}\<inverse>
[PROOF STEP]
by(blast intro: P_f)
[PROOF STATE]
proof (state)
this:
wf {(c', c). (P c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c f c) \<and> c' = c \<triangle>\<^sub>c f c}

goal (2 subgoals):
 1. \<And>s. \<lbrakk>P s; \<not> s \<sqsubseteq> s \<triangle>\<^sub>c f s\<rbrakk> \<Longrightarrow> P (s \<triangle>\<^sub>c f s)
 2. P c0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>P s; \<not> s \<sqsubseteq> s \<triangle>\<^sub>c f s\<rbrakk> \<Longrightarrow> P (s \<triangle>\<^sub>c f s)
 2. P c0
[PROOF STEP]
show "P c0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P c0
[PROOF STEP]
by(rule \<open>P c0\<close>)
[PROOF STATE]
proof (state)
this:
P c0

goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; \<not> s \<sqsubseteq> s \<triangle>\<^sub>c f s\<rbrakk> \<Longrightarrow> P (s \<triangle>\<^sub>c f s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; \<not> s \<sqsubseteq> s \<triangle>\<^sub>c f s\<rbrakk> \<Longrightarrow> P (s \<triangle>\<^sub>c f s)
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; \<not> s \<sqsubseteq> s \<triangle>\<^sub>c f s\<rbrakk> \<Longrightarrow> P (s \<triangle>\<^sub>c f s)
[PROOF STEP]
assume "P c"
[PROOF STATE]
proof (state)
this:
P c

goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; \<not> s \<sqsubseteq> s \<triangle>\<^sub>c f s\<rbrakk> \<Longrightarrow> P (s \<triangle>\<^sub>c f s)
[PROOF STEP]
thus "P (c \<triangle>\<^sub>c f c)"
[PROOF STATE]
proof (prove)
using this:
P c

goal (1 subgoal):
 1. P (c \<triangle>\<^sub>c f c)
[PROOF STEP]
by(simp add: P_f)
[PROOF STATE]
proof (state)
this:
P (c \<triangle>\<^sub>c f c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iter_winden_step_ivl_termination:
  "\<exists>c. iter_widen (step_ivl \<top>) (\<bottom>\<^sub>c c0) = Some c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. iter_widen (step_ivl \<top>) (\<bottom>\<^sub>c c0) = Some c
[PROOF STEP]
apply(rule iter_widen_termination[where
  P = "%c. strip c = c0 \<and> c : Com(vars c0)"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>c. strip c = c0 \<and> c \<in> Com (vars c0) \<Longrightarrow> strip (step_ivl \<top> c) = c0 \<and> step_ivl \<top> c \<in> Com (vars c0)
 2. \<And>c c'. \<lbrakk>strip c = c0 \<and> c \<in> Com (vars c0); strip c' = c0 \<and> c' \<in> Com (vars c0)\<rbrakk> \<Longrightarrow> strip (c \<nabla>\<^sub>c c') = c0 \<and> c \<nabla>\<^sub>c c' \<in> Com (vars c0)
 3. wf ({(c, c \<nabla>\<^sub>c c') |c c'. (strip c = c0 \<and> c \<in> Com (vars c0)) \<and> (strip c' = c0 \<and> c' \<in> Com (vars c0)) \<and> \<not> c' \<sqsubseteq> c}\<inverse>)
 4. strip (\<bottom>\<^sub>c c0) = c0 \<and> \<bottom>\<^sub>c c0 \<in> Com (vars c0)
 5. \<bottom>\<^sub>c c0 \<sqsubseteq> step_ivl \<top> (\<bottom>\<^sub>c c0)
[PROOF STEP]
apply (simp_all add: step'_Com bot_acom)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf ({(c, c \<nabla>\<^sub>c c') |c c'. strip c = c0 \<and> c \<in> Com (vars c0) \<and> strip c' = c0 \<and> c' \<in> Com (vars c0) \<and> \<not> c' \<sqsubseteq> c}\<inverse>)
[PROOF STEP]
apply(rule wf_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf ?r7
 2. {(c, c \<nabla>\<^sub>c c') |c c'. strip c = c0 \<and> c \<in> Com (vars c0) \<and> strip c' = c0 \<and> c' \<in> Com (vars c0) \<and> \<not> c' \<sqsubseteq> c}\<inverse> \<subseteq> ?r7
[PROOF STEP]
apply(rule wf_measure)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(c, c \<nabla>\<^sub>c c') |c c'. strip c = c0 \<and> c \<in> Com (vars c0) \<and> strip c' = c0 \<and> c' \<in> Com (vars c0) \<and> \<not> c' \<sqsubseteq> c}\<inverse> \<subseteq> measure ?f10
[PROOF STEP]
apply(rule subset_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {(c, c \<nabla>\<^sub>c c') |c c'. strip c = c0 \<and> c \<in> Com (vars c0) \<and> strip c' = c0 \<and> c' \<in> Com (vars c0) \<and> \<not> c' \<sqsubseteq> c}\<inverse> \<subseteq> ?B11
 2. ?B11 \<subseteq> measure ?f10
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ?B11 \<subseteq> measure ?f10
 2. {(c, c \<nabla>\<^sub>c c') |c c'. strip c = c0 \<and> c \<in> Com (vars c0) \<and> strip c' = c0 \<and> c' \<in> Com (vars c0) \<and> \<not> c' \<sqsubseteq> c}\<inverse> \<subseteq> ?B11
[PROOF STEP]
apply(rule measure_m_c[where X = "vars c0", OF finite_cvars])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(c, c \<nabla>\<^sub>c c') |c c'. strip c = c0 \<and> c \<in> Com (vars c0) \<and> strip c' = c0 \<and> c' \<in> Com (vars c0) \<and> \<not> c' \<sqsubseteq> c}\<inverse> \<subseteq> {(c, c \<nabla>\<^sub>c c') |c c'. strip c' = strip c \<and> c \<in> Com (vars c0) \<and> c' \<in> Com (vars c0) \<and> \<not> c' \<sqsubseteq> c}\<inverse>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iter_narrow_step_ivl_termination:
  "c0 \<in> Com (vars(strip c0)) \<Longrightarrow> step_ivl \<top> c0 \<sqsubseteq> c0 \<Longrightarrow>
  \<exists>c. iter_narrow (step_ivl \<top>) c0 = Some c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> \<exists>c. iter_narrow (step_ivl \<top>) c0 = Some c
[PROOF STEP]
apply(rule iter_narrow_termination[where
  P = "%c. strip c = strip c0 \<and> c : Com(vars(strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0; strip c = strip c0 \<and> c \<in> Com (vars (strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c\<rbrakk> \<Longrightarrow> strip (c \<triangle>\<^sub>c step_ivl \<top> c) = strip c0 \<and> c \<triangle>\<^sub>c step_ivl \<top> c \<in> Com (vars (strip c0)) \<and> step_ivl \<top> (c \<triangle>\<^sub>c step_ivl \<top> c) \<sqsubseteq> c \<triangle>\<^sub>c step_ivl \<top> c
 2. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> wf ({uu_. \<exists>c c'. uu_ = (c, c \<triangle>\<^sub>c step_ivl \<top> c) \<and> (strip c = strip c0 \<and> c \<in> Com (vars (strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c) \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c step_ivl \<top> c}\<inverse>)
 3. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> strip c0 = strip c0 \<and> c0 \<in> Com (vars (strip c0)) \<and> step_ivl \<top> c0 \<sqsubseteq> c0
[PROOF STEP]
apply (simp_all add: step'_Com)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0; strip c = strip c0 \<and> c \<in> Com (vars (strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c\<rbrakk> \<Longrightarrow> step_ivl \<top> (c \<triangle>\<^sub>c step_ivl \<top> c) \<sqsubseteq> c \<triangle>\<^sub>c step_ivl \<top> c
 2. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> wf ({(c, c \<triangle>\<^sub>c step_ivl \<top> c) |c. strip c = strip c0 \<and> c \<in> Com (vars (strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c step_ivl \<top> c}\<inverse>)
[PROOF STEP]
apply(clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0; strip c = strip c0; c \<in> Com (vars (strip c0)); step_ivl \<top> c \<sqsubseteq> c\<rbrakk> \<Longrightarrow> step_ivl \<top> (c \<triangle>\<^sub>c step_ivl \<top> c) \<sqsubseteq> c \<triangle>\<^sub>c step_ivl \<top> c
 2. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> wf ({(c, c \<triangle>\<^sub>c step_ivl \<top> c) |c. strip c = strip c0 \<and> c \<in> Com (vars (strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c step_ivl \<top> c}\<inverse>)
[PROOF STEP]
apply(frule narrow2_acom, drule mono_step'[OF le_refl], erule le_trans[OF _ narrow1_acom])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0; strip c = strip c0; c \<in> Com (vars (strip c0)); step_ivl \<top> c \<sqsubseteq> c\<rbrakk> \<Longrightarrow> step_ivl \<top> c \<sqsubseteq> c
 2. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> wf ({(c, c \<triangle>\<^sub>c step_ivl \<top> c) |c. strip c = strip c0 \<and> c \<in> Com (vars (strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c step_ivl \<top> c}\<inverse>)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> wf ({(c, c \<triangle>\<^sub>c step_ivl \<top> c) |c. strip c = strip c0 \<and> c \<in> Com (vars (strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c step_ivl \<top> c}\<inverse>)
[PROOF STEP]
apply(rule wf_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> wf ?r16
 2. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> {(c, c \<triangle>\<^sub>c step_ivl \<top> c) |c. strip c = strip c0 \<and> c \<in> Com (vars (strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c step_ivl \<top> c}\<inverse> \<subseteq> ?r16
[PROOF STEP]
apply(rule wf_measure)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> {(c, c \<triangle>\<^sub>c step_ivl \<top> c) |c. strip c = strip c0 \<and> c \<in> Com (vars (strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c step_ivl \<top> c}\<inverse> \<subseteq> measure ?f19
[PROOF STEP]
apply(rule subset_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> {(c, c \<triangle>\<^sub>c step_ivl \<top> c) |c. strip c = strip c0 \<and> c \<in> Com (vars (strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c step_ivl \<top> c}\<inverse> \<subseteq> ?B20
 2. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> ?B20 \<subseteq> measure ?f19
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> ?B20 \<subseteq> measure ?f19
 2. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> {(c, c \<triangle>\<^sub>c step_ivl \<top> c) |c. strip c = strip c0 \<and> c \<in> Com (vars (strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c step_ivl \<top> c}\<inverse> \<subseteq> ?B20
[PROOF STEP]
apply(rule measure_n_c[where X = "vars(strip c0)", OF finite_cvars])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> {(c, c \<triangle>\<^sub>c step_ivl \<top> c) |c. strip c = strip c0 \<and> c \<in> Com (vars (strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c step_ivl \<top> c}\<inverse> \<subseteq> {(c, c \<triangle>\<^sub>c c') |c c'. strip c = strip c' \<and> c \<in> Com (vars (strip c0)) \<and> c' \<in> Com (vars (strip c0)) \<and> c' \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'}\<inverse>
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>c0 \<in> Com (vars (strip c0)); step_ivl \<top> c0 \<sqsubseteq> c0; strip c = strip c0; c \<in> Com (vars (strip c0)); step_ivl \<top> c \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c step_ivl \<top> c\<rbrakk> \<Longrightarrow> \<exists>c'. c \<triangle>\<^sub>c step_ivl \<top> c = c \<triangle>\<^sub>c c' \<and> strip c0 = strip c' \<and> c' \<in> Com (vars (strip c0)) \<and> c' \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'
[PROOF STEP]
by (metis bot_least domo_Top order_refl step'_Com strip_step')


[STATEMENT]
lemma while_Com:
fixes c :: "'a st option acom"
assumes "while_option P f c = Some c'"
and "!!c. strip(f c) = strip c"
and "\<forall>c::'a st option acom. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> f c : Com(X)"
and "c : Com(X)" and "vars(strip c) \<subseteq> X" shows "c' : Com(X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c' \<in> Com X
[PROOF STEP]
using while_option_rule[where P = "\<lambda>c'. c' : Com(X) \<and> vars(strip c') \<subseteq> X", OF _ assms(1)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>s. \<lbrakk>s \<in> Com X \<and> vars (strip s) \<subseteq> X; P s\<rbrakk> \<Longrightarrow> f s \<in> Com X \<and> vars (strip (f s)) \<subseteq> X; c \<in> Com X \<and> vars (strip c) \<subseteq> X\<rbrakk> \<Longrightarrow> c' \<in> Com X \<and> vars (strip c') \<subseteq> X

goal (1 subgoal):
 1. c' \<in> Com X
[PROOF STEP]
by(simp add: assms(2-))


[STATEMENT]
lemma iter_widen_Com: fixes f :: "'a::WN st option acom \<Rightarrow> 'a st option acom"
assumes "iter_widen f c = Some c'"
and "\<forall>c. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> f c : Com(X)"
and "!!c. strip(f c) = strip c"
and "c : Com(X)" and "vars (strip c) \<subseteq> X" shows "c' : Com(X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c' \<in> Com X
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c' \<in> Com X
[PROOF STEP]
have "\<forall>c. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> c \<nabla>\<^sub>c f c : Com(X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. c \<in> Com X \<longrightarrow> vars (strip c) \<subseteq> X \<longrightarrow> c \<nabla>\<^sub>c f c \<in> Com X
[PROOF STEP]
by (metis (full_types) widen_acom_Com assms(2,3))
[PROOF STATE]
proof (state)
this:
\<forall>c. c \<in> Com X \<longrightarrow> vars (strip c) \<subseteq> X \<longrightarrow> c \<nabla>\<^sub>c f c \<in> Com X

goal (1 subgoal):
 1. c' \<in> Com X
[PROOF STEP]
from while_Com[OF assms(1)[simplified iter_widen_def] _ this assms(4,5)]
[PROOF STATE]
proof (chain)
picking this:
(\<And>c. strip (c \<nabla>\<^sub>c f c) = strip c) \<Longrightarrow> c' \<in> Com X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>c. strip (c \<nabla>\<^sub>c f c) = strip c) \<Longrightarrow> c' \<in> Com X

goal (1 subgoal):
 1. c' \<in> Com X
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
(\<And>c. strip (c \<nabla>\<^sub>c f c) = strip c) \<Longrightarrow> c' \<in> Com X
strip (f ?c) = strip ?c

goal (1 subgoal):
 1. c' \<in> Com X
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
c' \<in> Com X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iter_widen_step'_Com:
  "iter_widen (step' \<top>) c = Some c' \<Longrightarrow> vars(strip c) \<subseteq> X \<Longrightarrow> c : Com(X)
   \<Longrightarrow> c' : Com(X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>iter_widen (local.step' \<top>) c = Some c'; vars (strip c) \<subseteq> X; c \<in> Com X\<rbrakk> \<Longrightarrow> c' \<in> Com X
[PROOF STEP]
apply(subgoal_tac "strip c'= strip c")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>iter_widen (local.step' \<top>) c = Some c'; vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> c' \<in> Com X
 2. \<lbrakk>iter_widen (local.step' \<top>) c = Some c'; vars (strip c) \<subseteq> X; c \<in> Com X\<rbrakk> \<Longrightarrow> strip c' = strip c
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>iter_widen (local.step' \<top>) c = Some c'; vars (strip c) \<subseteq> X; c \<in> Com X\<rbrakk> \<Longrightarrow> strip c' = strip c
 2. \<lbrakk>iter_widen (local.step' \<top>) c = Some c'; vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> c' \<in> Com X
[PROOF STEP]
apply (metis strip_iter_widen strip_step')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>iter_widen (local.step' \<top>) c = Some c'; vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> c' \<in> Com X
[PROOF STEP]
apply(drule iter_widen_Com)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> \<forall>c. c \<in> Com ?X5 \<longrightarrow> vars (strip c) \<subseteq> ?X5 \<longrightarrow> local.step' \<top> c \<in> Com ?X5
 2. \<And>ca. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> strip (local.step' \<top> ca) = strip ca
 3. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> c \<in> Com ?X5
 4. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> vars (strip c) \<subseteq> ?X5
 5. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c; c' \<in> Com ?X5\<rbrakk> \<Longrightarrow> c' \<in> Com X
[PROOF STEP]
prefer 3
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> c \<in> Com ?X5
 2. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> \<forall>c. c \<in> Com ?X5 \<longrightarrow> vars (strip c) \<subseteq> ?X5 \<longrightarrow> local.step' \<top> c \<in> Com ?X5
 3. \<And>ca. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> strip (local.step' \<top> ca) = strip ca
 4. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> vars (strip c) \<subseteq> ?X5
 5. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c; c' \<in> Com ?X5\<rbrakk> \<Longrightarrow> c' \<in> Com X
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> \<forall>c. c \<in> Com X \<longrightarrow> vars (strip c) \<subseteq> X \<longrightarrow> local.step' \<top> c \<in> Com X
 2. \<And>ca. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> strip (local.step' \<top> ca) = strip ca
 3. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> vars (strip c) \<subseteq> X
 4. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c; c' \<in> Com X\<rbrakk> \<Longrightarrow> c' \<in> Com X
[PROOF STEP]
prefer 3
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> vars (strip c) \<subseteq> X
 2. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> \<forall>c. c \<in> Com X \<longrightarrow> vars (strip c) \<subseteq> X \<longrightarrow> local.step' \<top> c \<in> Com X
 3. \<And>ca. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> strip (local.step' \<top> ca) = strip ca
 4. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c; c' \<in> Com X\<rbrakk> \<Longrightarrow> c' \<in> Com X
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> \<forall>c. c \<in> Com X \<longrightarrow> vars (strip c) \<subseteq> X \<longrightarrow> local.step' \<top> c \<in> Com X
 2. \<And>ca. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c\<rbrakk> \<Longrightarrow> strip (local.step' \<top> ca) = strip ca
 3. \<lbrakk>vars (strip c) \<subseteq> X; c \<in> Com X; strip c' = strip c; c' \<in> Com X\<rbrakk> \<Longrightarrow> c' \<in> Com X
[PROOF STEP]
apply (auto simp: step'_Com)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem AI_ivl'_termination:
  "\<exists>c'. AI_ivl' c = Some c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c'. AI_ivl' c = Some c'
[PROOF STEP]
apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination split: option.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2. iter_widen (step_ivl \<top>) (\<bottom>\<^sub>c c) = Some x2 \<Longrightarrow> \<exists>c'. iter_narrow (step_ivl \<top>) x2 = Some c'
[PROOF STEP]
apply(rule iter_narrow_step_ivl_termination)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x2. iter_widen (step_ivl \<top>) (\<bottom>\<^sub>c c) = Some x2 \<Longrightarrow> x2 \<in> Com (vars (strip x2))
 2. \<And>x2. iter_widen (step_ivl \<top>) (\<bottom>\<^sub>c c) = Some x2 \<Longrightarrow> step_ivl \<top> x2 \<sqsubseteq> x2
[PROOF STEP]
apply (metis bot_acom_Com iter_widen_step'_Com[OF _ subset_refl] strip_iter_widen strip_step')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2. iter_widen (step_ivl \<top>) (\<bottom>\<^sub>c c) = Some x2 \<Longrightarrow> step_ivl \<top> x2 \<sqsubseteq> x2
[PROOF STEP]
apply(erule iter_widen_pfp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ik_trans_ik_increasing: "(s, s') \<in> ik_trans \<Longrightarrow> ik s \<subseteq> ik s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> ik_trans \<Longrightarrow> ik s \<subseteq> ik s'
[PROOF STEP]
by (auto simp add: ik_trans_defs)


[STATEMENT]
lemma ik_trans_synth_analz_ik_increasing:
  "(s, s') \<in> ik_trans \<Longrightarrow> synth (analz (ik s)) \<subseteq> synth (analz (ik s'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> ik_trans \<Longrightarrow> synth (analz (ik s)) \<subseteq> synth (analz (ik s'))
[PROOF STEP]
by (simp only: synth_analz_mono ik_trans_ik_increasing)


[STATEMENT]
lemma check_certD [intro?]:
  "check_cert P mxs mxl n cert \<Longrightarrow> cert_ok cert n Err (OK None) (states P mxs mxl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_cert P mxs mxl n cert \<Longrightarrow> cert_ok cert n Err (OK None) (states P mxs mxl)
[PROOF STEP]
by (unfold cert_ok_def check_cert_def check_types_def) auto


[STATEMENT]
lemma (in start_context) wt_lbv_wt_step:
  assumes lbv: "wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is"
  shows "\<exists>\<tau>s \<in> nlists (size is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^sub>r \<tau>s!0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
from wf
[PROOF STATE]
proof (chain)
picking this:
wf_prog p P
[PROOF STEP]
have "semilat (JVM_SemiType.sl P mxs mxl)"
[PROOF STATE]
proof (prove)
using this:
wf_prog p P

goal (1 subgoal):
 1. semilat (JVM_SemiType.sl P mxs mxl)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
semilat (JVM_SemiType.sl P mxs mxl)

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
hence "semilat (A, r, f)"
[PROOF STATE]
proof (prove)
using this:
semilat (JVM_SemiType.sl P mxs mxl)

goal (1 subgoal):
 1. semilat (A, r, f)
[PROOF STEP]
by (simp add: sl_def2)
[PROOF STATE]
proof (state)
this:
semilat (A, r, f)

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
semilat (A, r, f)

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
have "top r Err"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Semilat.top r Err
[PROOF STEP]
by (simp add: JVM_le_Err_conv)
[PROOF STATE]
proof (state)
this:
Semilat.top r Err

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Semilat.top r Err

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
have "Err \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Err \<in> A
[PROOF STEP]
by (simp add: JVM_states_unfold)
[PROOF STATE]
proof (state)
this:
Err \<in> A

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Err \<in> A

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
have "bottom r (OK None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bottom r (OK None)
[PROOF STEP]
by (simp add: JVM_le_Err_conv bottom_def lesub_def Err.le_def split: err.split)
[PROOF STATE]
proof (state)
this:
bottom r (OK None)

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bottom r (OK None)

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
have "OK None \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK None \<in> A
[PROOF STEP]
by (simp add: JVM_states_unfold)
[PROOF STATE]
proof (state)
this:
OK None \<in> A

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
OK None \<in> A

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
note bounded_step
[PROOF STATE]
proof (state)
this:
bounded step (length is)

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bounded step (length is)

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
from lbv
[PROOF STATE]
proof (chain)
picking this:
wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
have "cert_ok cert (size is) Err (OK None) A"
[PROOF STATE]
proof (prove)
using this:
wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is

goal (1 subgoal):
 1. cert_ok cert (length is) Err (OK None) A
[PROOF STEP]
by (unfold wt_lbv_def) (auto dest: check_certD)
[PROOF STATE]
proof (state)
this:
cert_ok cert (length is) Err (OK None) A

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cert_ok cert (length is) Err (OK None) A

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
note exec_pres_type
[PROOF STATE]
proof (state)
this:
pres_type step (length is) A

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pres_type step (length is) A

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
from lbv
[PROOF STATE]
proof (chain)
picking this:
wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
have "wtl_inst_list is cert f r Err (OK None) step 0 (OK first) \<noteq> Err"
[PROOF STATE]
proof (prove)
using this:
wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is

goal (1 subgoal):
 1. wtl_inst_list is cert f r Err (OK None) step 0 (OK first) \<noteq> Err
[PROOF STEP]
by (cases b; simp add: wt_lbv_def lbvjvm_def step_def_exec [symmetric])
[PROOF STATE]
proof (state)
this:
wtl_inst_list is cert f r Err (OK None) step 0 (OK first) \<noteq> Err

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wtl_inst_list is cert f r Err (OK None) step 0 (OK first) \<noteq> Err

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
note first_in_A
[PROOF STATE]
proof (state)
this:
OK first \<in> A

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
OK first \<in> A

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
from lbv
[PROOF STATE]
proof (chain)
picking this:
wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
have "0 < size is"
[PROOF STATE]
proof (prove)
using this:
wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is

goal (1 subgoal):
 1. 0 < length is
[PROOF STEP]
by (simp add: wt_lbv_def)
[PROOF STATE]
proof (state)
this:
0 < length is

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
semilat (A, r, f)
Semilat.top r Err
Err \<in> A
bottom r (OK None)
OK None \<in> A
bounded step (length is)
cert_ok cert (length is) Err (OK None) A
pres_type step (length is) A
wtl_inst_list is cert f r Err (OK None) step 0 (OK first) \<noteq> Err
OK first \<in> A
0 < length is
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
semilat (A, r, f)
Semilat.top r Err
Err \<in> A
bottom r (OK None)
OK None \<in> A
bounded step (length is)
cert_ok cert (length is) Err (OK None) A
pres_type step (length is) A
wtl_inst_list is cert f r Err (OK None) step 0 (OK first) \<noteq> Err
OK first \<in> A
0 < length is

goal (1 subgoal):
 1. \<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
[PROOF STEP]
by (rule lbvs.wtl_sound_strong [OF lbvs.intro, OF lbv.intro lbvs_axioms.intro, OF Semilat.intro lbv_axioms.intro])
[PROOF STATE]
proof (state)
this:
\<exists>\<tau>s\<in>nlists (length is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in start_context) wt_lbv_wt_method:
  assumes lbv: "wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is"
  shows "\<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
from lbv
[PROOF STATE]
proof (chain)
picking this:
wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
have l: "is \<noteq> []" and
             stab: "b = Static \<or> b = NonStatic"
[PROOF STATE]
proof (prove)
using this:
wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is

goal (1 subgoal):
 1. is \<noteq> [] &&& b = Static \<or> b = NonStatic
[PROOF STEP]
by (auto simp add: wt_lbv_def)
[PROOF STATE]
proof (state)
this:
is \<noteq> []
b = Static \<or> b = NonStatic

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is \<noteq> []
b = Static \<or> b = NonStatic

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
from wf lbv C Ts
[PROOF STATE]
proof (chain)
picking this:
wf_prog p P
wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
is_class P C
set Ts \<subseteq> types P
[PROOF STEP]
obtain \<tau>s where
    list:  "\<tau>s \<in> nlists (size is) A" and
    step:  "wt_step r Err step \<tau>s" and
    start: "OK first \<sqsubseteq>\<^sub>r \<tau>s!0"
[PROOF STATE]
proof (prove)
using this:
wf_prog p P
wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
is_class P C
set Ts \<subseteq> types P

goal (1 subgoal):
 1. (\<And>\<tau>s. \<lbrakk>\<tau>s \<in> nlists (length is) A; wt_step r Err step \<tau>s; OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast dest: wt_lbv_wt_step)
[PROOF STATE]
proof (state)
this:
\<tau>s \<in> nlists (length is) A
wt_step r Err step \<tau>s
OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
from list
[PROOF STATE]
proof (chain)
picking this:
\<tau>s \<in> nlists (length is) A
[PROOF STEP]
have [simp]: "size \<tau>s = size is"
[PROOF STATE]
proof (prove)
using this:
\<tau>s \<in> nlists (length is) A

goal (1 subgoal):
 1. length \<tau>s = length is
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length \<tau>s = length is

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
have "size (map ok_val \<tau>s) = size is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map ok_val \<tau>s) = length is
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (map ok_val \<tau>s) = length is

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (map ok_val \<tau>s) = length is

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
from l
[PROOF STATE]
proof (chain)
picking this:
is \<noteq> []
[PROOF STEP]
have 0: "0 < size \<tau>s"
[PROOF STATE]
proof (prove)
using this:
is \<noteq> []

goal (1 subgoal):
 1. 0 < length \<tau>s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < length \<tau>s

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
with step
[PROOF STATE]
proof (chain)
picking this:
wt_step r Err step \<tau>s
0 < length \<tau>s
[PROOF STEP]
obtain \<tau>s0 where "\<tau>s!0 = OK \<tau>s0"
[PROOF STATE]
proof (prove)
using this:
wt_step r Err step \<tau>s
0 < length \<tau>s

goal (1 subgoal):
 1. (\<And>\<tau>s0. \<tau>s ! 0 = OK \<tau>s0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (unfold wt_step_def) blast
[PROOF STATE]
proof (state)
this:
\<tau>s ! 0 = OK \<tau>s0

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
with start 0
[PROOF STATE]
proof (chain)
picking this:
OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
0 < length \<tau>s
\<tau>s ! 0 = OK \<tau>s0
[PROOF STEP]
have "wt_start P C b Ts mxl\<^sub>0 (map ok_val \<tau>s)"
[PROOF STATE]
proof (prove)
using this:
OK first \<sqsubseteq>\<^bsub>r\<^esub> \<tau>s ! 0
0 < length \<tau>s
\<tau>s ! 0 = OK \<tau>s0

goal (1 subgoal):
 1. wt_start P C b Ts mxl\<^sub>0 (map ok_val \<tau>s)
[PROOF STEP]
by (cases b; simp add: wt_start_def JVM_le_Err_conv lesub_def Err.le_def)
[PROOF STATE]
proof (state)
this:
wt_start P C b Ts mxl\<^sub>0 (map ok_val \<tau>s)

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wt_start P C b Ts mxl\<^sub>0 (map ok_val \<tau>s)

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
wt_start P C b Ts mxl\<^sub>0 (map ok_val \<tau>s)

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
from list
[PROOF STATE]
proof (chain)
picking this:
\<tau>s \<in> nlists (length is) A
[PROOF STEP]
have "check_types P mxs mxl \<tau>s"
[PROOF STATE]
proof (prove)
using this:
\<tau>s \<in> nlists (length is) A

goal (1 subgoal):
 1. check_types P mxs mxl \<tau>s
[PROOF STEP]
by (simp add: check_types_def)
[PROOF STATE]
proof (state)
this:
check_types P mxs mxl \<tau>s

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
check_types P mxs mxl \<tau>s

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
from step
[PROOF STATE]
proof (chain)
picking this:
wt_step r Err step \<tau>s
[PROOF STEP]
have "\<forall>x \<in> set \<tau>s. x \<noteq> Err"
[PROOF STATE]
proof (prove)
using this:
wt_step r Err step \<tau>s

goal (1 subgoal):
 1. \<forall>x\<in>set \<tau>s. x \<noteq> Err
[PROOF STEP]
by (auto simp add: all_set_conv_all_nth wt_step_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set \<tau>s. x \<noteq> Err

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
hence [symmetric]: "map OK (map ok_val \<tau>s) = \<tau>s"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set \<tau>s. x \<noteq> Err

goal (1 subgoal):
 1. map OK (map ok_val \<tau>s) = \<tau>s
[PROOF STEP]
by (auto intro!: map_idI)
[PROOF STATE]
proof (state)
this:
\<tau>s = map OK (map ok_val \<tau>s)

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
check_types P mxs mxl (map OK (map ok_val \<tau>s))
[PROOF STEP]
have "check_types P mxs mxl (map OK (map ok_val \<tau>s))"
[PROOF STATE]
proof (prove)
using this:
check_types P mxs mxl (map OK (map ok_val \<tau>s))

goal (1 subgoal):
 1. check_types P mxs mxl (map OK (map ok_val \<tau>s))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
check_types P mxs mxl (map OK (map ok_val \<tau>s))

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
check_types P mxs mxl (map OK (map ok_val \<tau>s))

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
check_types P mxs mxl (map OK (map ok_val \<tau>s))

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
check_types P mxs mxl (map OK (map ok_val \<tau>s))

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
note bounded_step
[PROOF STATE]
proof (state)
this:
bounded step (length is)

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bounded step (length is)

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
from list
[PROOF STATE]
proof (chain)
picking this:
\<tau>s \<in> nlists (length is) A
[PROOF STEP]
have "set \<tau>s \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
\<tau>s \<in> nlists (length is) A

goal (1 subgoal):
 1. set \<tau>s \<subseteq> A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set \<tau>s \<subseteq> A

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set \<tau>s \<subseteq> A

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
from step
[PROOF STATE]
proof (chain)
picking this:
wt_step r Err step \<tau>s
[PROOF STEP]
have "wt_err_step (sup_state_opt P) step \<tau>s"
[PROOF STATE]
proof (prove)
using this:
wt_step r Err step \<tau>s

goal (1 subgoal):
 1. wt_err_step (sup_state_opt P) step \<tau>s
[PROOF STEP]
by (simp add: wt_err_step_def JVM_le_Err_conv)
[PROOF STATE]
proof (state)
this:
wt_err_step (sup_state_opt P) step \<tau>s

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bounded step (length is)
set \<tau>s \<subseteq> A
wt_err_step (sup_state_opt P) step \<tau>s
[PROOF STEP]
have "wt_app_eff (sup_state_opt P) app eff (map ok_val \<tau>s)"
[PROOF STATE]
proof (prove)
using this:
bounded step (length is)
set \<tau>s \<subseteq> A
wt_err_step (sup_state_opt P) step \<tau>s

goal (1 subgoal):
 1. wt_app_eff (sup_state_opt P) app eff (map ok_val \<tau>s)
[PROOF STEP]
by (auto intro: wt_err_imp_wt_app_eff simp add: exec_def states_def)
[PROOF STATE]
proof (state)
this:
wt_app_eff (sup_state_opt P) app eff (map ok_val \<tau>s)

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
wt_app_eff (sup_state_opt P) app eff (map ok_val \<tau>s)

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is \<noteq> []
b = Static \<or> b = NonStatic
length (map ok_val \<tau>s) = length is
wt_start P C b Ts mxl\<^sub>0 (map ok_val \<tau>s)
check_types P mxs mxl (map OK (map ok_val \<tau>s))
wt_app_eff (sup_state_opt P) app eff (map ok_val \<tau>s)
[PROOF STEP]
have "wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (map ok_val \<tau>s)"
[PROOF STATE]
proof (prove)
using this:
is \<noteq> []
b = Static \<or> b = NonStatic
length (map ok_val \<tau>s) = length is
wt_start P C b Ts mxl\<^sub>0 (map ok_val \<tau>s)
check_types P mxs mxl (map OK (map ok_val \<tau>s))
wt_app_eff (sup_state_opt P) app eff (map ok_val \<tau>s)

goal (1 subgoal):
 1. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (map ok_val \<tau>s)
[PROOF STEP]
by (simp add: wt_method_def2 check_types_def del: map_map)
[PROOF STATE]
proof (state)
this:
wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (map ok_val \<tau>s)

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (map ok_val \<tau>s)

goal (1 subgoal):
 1. \<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in start_context) wt_method_wt_lbv:
  assumes wt: "wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
  defines [simp]: "cert \<equiv> mk_cert P mxs T\<^sub>r xt is \<tau>s"

  shows "wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
let ?\<tau>s  = "map OK \<tau>s"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
let ?cert = "make_cert step ?\<tau>s (OK None)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
from wt
[PROOF STATE]
proof (chain)
picking this:
wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s
[PROOF STEP]
obtain
    0:        "0 < size is" and
    size:     "size is = size ?\<tau>s" and
    ck_types: "check_types P mxs mxl ?\<tau>s" and
    wt_start: "wt_start P C b Ts mxl\<^sub>0 \<tau>s" and
    app_eff:  "wt_app_eff (sup_state_opt P) app eff \<tau>s"
[PROOF STATE]
proof (prove)
using this:
wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s

goal (1 subgoal):
 1. (\<lbrakk>0 < length is; length is = length (map OK \<tau>s); check_types P mxs mxl (map OK \<tau>s); wt_start P C b Ts mxl\<^sub>0 \<tau>s; wt_app_eff (sup_state_opt P) app eff \<tau>s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (force simp add: wt_method_def2 check_types_def)
[PROOF STATE]
proof (state)
this:
0 < length is
length is = length (map OK \<tau>s)
check_types P mxs mxl (map OK \<tau>s)
wt_start P C b Ts mxl\<^sub>0 \<tau>s
wt_app_eff (sup_state_opt P) app eff \<tau>s

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
from wf
[PROOF STATE]
proof (chain)
picking this:
wf_prog p P
[PROOF STEP]
have "semilat (JVM_SemiType.sl P mxs mxl)"
[PROOF STATE]
proof (prove)
using this:
wf_prog p P

goal (1 subgoal):
 1. semilat (JVM_SemiType.sl P mxs mxl)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
semilat (JVM_SemiType.sl P mxs mxl)

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
hence "semilat (A, r, f)"
[PROOF STATE]
proof (prove)
using this:
semilat (JVM_SemiType.sl P mxs mxl)

goal (1 subgoal):
 1. semilat (A, r, f)
[PROOF STEP]
by (simp add: sl_def2)
[PROOF STATE]
proof (state)
this:
semilat (A, r, f)

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
semilat (A, r, f)

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
have "top r Err"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Semilat.top r Err
[PROOF STEP]
by (simp add: JVM_le_Err_conv)
[PROOF STATE]
proof (state)
this:
Semilat.top r Err

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Semilat.top r Err

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
have "Err \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Err \<in> A
[PROOF STEP]
by (simp add: JVM_states_unfold)
[PROOF STATE]
proof (state)
this:
Err \<in> A

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Err \<in> A

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
have "bottom r (OK None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bottom r (OK None)
[PROOF STEP]
by (simp add: JVM_le_Err_conv bottom_def lesub_def Err.le_def split: err.split)
[PROOF STATE]
proof (state)
this:
bottom r (OK None)

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bottom r (OK None)

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
have "OK None \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK None \<in> A
[PROOF STEP]
by (simp add: JVM_states_unfold)
[PROOF STATE]
proof (state)
this:
OK None \<in> A

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
OK None \<in> A

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
from wf
[PROOF STATE]
proof (chain)
picking this:
wf_prog p P
[PROOF STEP]
have "mono r step (size is) A"
[PROOF STATE]
proof (prove)
using this:
wf_prog p P

goal (1 subgoal):
 1. SemilatAlg.mono r step (length is) A
[PROOF STEP]
by (rule step_mono)
[PROOF STATE]
proof (state)
this:
SemilatAlg.mono r step (length is) A

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
hence "mono r step (size ?\<tau>s) A"
[PROOF STATE]
proof (prove)
using this:
SemilatAlg.mono r step (length is) A

goal (1 subgoal):
 1. SemilatAlg.mono r step (length (map OK \<tau>s)) A
[PROOF STEP]
by (simp add: size)
[PROOF STATE]
proof (state)
this:
SemilatAlg.mono r step (length (map OK \<tau>s)) A

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
SemilatAlg.mono r step (length (map OK \<tau>s)) A

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
from exec_pres_type
[PROOF STATE]
proof (chain)
picking this:
pres_type step (length is) A
[PROOF STEP]
have "pres_type step (size ?\<tau>s) A"
[PROOF STATE]
proof (prove)
using this:
pres_type step (length is) A

goal (1 subgoal):
 1. pres_type step (length (map OK \<tau>s)) A
[PROOF STEP]
by (simp add: size)
[PROOF STATE]
proof (state)
this:
pres_type step (length (map OK \<tau>s)) A

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pres_type step (length (map OK \<tau>s)) A

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
from ck_types
[PROOF STATE]
proof (chain)
picking this:
check_types P mxs mxl (map OK \<tau>s)
[PROOF STEP]
have \<tau>s_in_A: "set ?\<tau>s \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
check_types P mxs mxl (map OK \<tau>s)

goal (1 subgoal):
 1. set (map OK \<tau>s) \<subseteq> A
[PROOF STEP]
by (simp add: check_types_def)
[PROOF STATE]
proof (state)
this:
set (map OK \<tau>s) \<subseteq> A

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
hence "\<forall>pc. pc < size ?\<tau>s \<longrightarrow> ?\<tau>s!pc \<in> A \<and> ?\<tau>s!pc \<noteq> Err"
[PROOF STATE]
proof (prove)
using this:
set (map OK \<tau>s) \<subseteq> A

goal (1 subgoal):
 1. \<forall>pc<length (map OK \<tau>s). map OK \<tau>s ! pc \<in> A \<and> map OK \<tau>s ! pc \<noteq> Err
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>pc<length (map OK \<tau>s). map OK \<tau>s ! pc \<in> A \<and> map OK \<tau>s ! pc \<noteq> Err

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>pc<length (map OK \<tau>s). map OK \<tau>s ! pc \<in> A \<and> map OK \<tau>s ! pc \<noteq> Err

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
from bounded_step
[PROOF STATE]
proof (chain)
picking this:
bounded step (length is)
[PROOF STEP]
have "bounded step (size ?\<tau>s)"
[PROOF STATE]
proof (prove)
using this:
bounded step (length is)

goal (1 subgoal):
 1. bounded step (length (map OK \<tau>s))
[PROOF STEP]
by (simp add: size)
[PROOF STATE]
proof (state)
this:
bounded step (length (map OK \<tau>s))

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bounded step (length (map OK \<tau>s))

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
have "OK None \<noteq> Err"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK None \<noteq> Err
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
OK None \<noteq> Err

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
OK None \<noteq> Err

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
from bounded_step size \<tau>s_in_A app_eff
[PROOF STATE]
proof (chain)
picking this:
bounded step (length is)
length is = length (map OK \<tau>s)
set (map OK \<tau>s) \<subseteq> A
wt_app_eff (sup_state_opt P) app eff \<tau>s
[PROOF STEP]
have "wt_err_step (sup_state_opt P) step ?\<tau>s"
[PROOF STATE]
proof (prove)
using this:
bounded step (length is)
length is = length (map OK \<tau>s)
set (map OK \<tau>s) \<subseteq> A
wt_app_eff (sup_state_opt P) app eff \<tau>s

goal (1 subgoal):
 1. wt_err_step (sup_state_opt P) step (map OK \<tau>s)
[PROOF STEP]
by (auto intro: wt_app_eff_imp_wt_err simp add: exec_def states_def)
[PROOF STATE]
proof (state)
this:
wt_err_step (sup_state_opt P) step (map OK \<tau>s)

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
hence "wt_step r Err step ?\<tau>s"
[PROOF STATE]
proof (prove)
using this:
wt_err_step (sup_state_opt P) step (map OK \<tau>s)

goal (1 subgoal):
 1. wt_step r Err step (map OK \<tau>s)
[PROOF STEP]
by (simp add: wt_err_step_def JVM_le_Err_conv)
[PROOF STATE]
proof (state)
this:
wt_step r Err step (map OK \<tau>s)

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wt_step r Err step (map OK \<tau>s)

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
from 0 size
[PROOF STATE]
proof (chain)
picking this:
0 < length is
length is = length (map OK \<tau>s)
[PROOF STEP]
have "0 < size \<tau>s"
[PROOF STATE]
proof (prove)
using this:
0 < length is
length is = length (map OK \<tau>s)

goal (1 subgoal):
 1. 0 < length \<tau>s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < length \<tau>s

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
hence "?\<tau>s!0 = OK (\<tau>s!0)"
[PROOF STATE]
proof (prove)
using this:
0 < length \<tau>s

goal (1 subgoal):
 1. map OK \<tau>s ! 0 = OK (\<tau>s ! 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map OK \<tau>s ! 0 = OK (\<tau>s ! 0)

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
with wt_start
[PROOF STATE]
proof (chain)
picking this:
wt_start P C b Ts mxl\<^sub>0 \<tau>s
map OK \<tau>s ! 0 = OK (\<tau>s ! 0)
[PROOF STEP]
have "OK first \<sqsubseteq>\<^sub>r ?\<tau>s!0"
[PROOF STATE]
proof (prove)
using this:
wt_start P C b Ts mxl\<^sub>0 \<tau>s
map OK \<tau>s ! 0 = OK (\<tau>s ! 0)

goal (1 subgoal):
 1. OK first \<sqsubseteq>\<^bsub>r\<^esub> map OK \<tau>s ! 0
[PROOF STEP]
by (cases b; clarsimp simp add: wt_start_def lesub_def Err.le_def JVM_le_Err_conv)
[PROOF STATE]
proof (state)
this:
OK first \<sqsubseteq>\<^bsub>r\<^esub> map OK \<tau>s ! 0

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
OK first \<sqsubseteq>\<^bsub>r\<^esub> map OK \<tau>s ! 0

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
note first_in_A
[PROOF STATE]
proof (state)
this:
OK first \<in> A

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
OK first \<in> A

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
have "OK first \<noteq> Err"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK first \<noteq> Err
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
OK first \<noteq> Err

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
OK first \<noteq> Err

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
note size
[PROOF STATE]
proof (state)
this:
length is = length (map OK \<tau>s)

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
semilat (A, r, f)
Semilat.top r Err
Err \<in> A
bottom r (OK None)
OK None \<in> A
SemilatAlg.mono r step (length (map OK \<tau>s)) A
pres_type step (length (map OK \<tau>s)) A
\<forall>pc<length (map OK \<tau>s). map OK \<tau>s ! pc \<in> A \<and> map OK \<tau>s ! pc \<noteq> Err
bounded step (length (map OK \<tau>s))
OK None \<noteq> Err
wt_step r Err step (map OK \<tau>s)
OK first \<sqsubseteq>\<^bsub>r\<^esub> map OK \<tau>s ! 0
OK first \<in> A
OK first \<noteq> Err
length is = length (map OK \<tau>s)
[PROOF STEP]
have "wtl_inst_list is ?cert f r Err (OK None) step 0 (OK first) \<noteq> Err"
[PROOF STATE]
proof (prove)
using this:
semilat (A, r, f)
Semilat.top r Err
Err \<in> A
bottom r (OK None)
OK None \<in> A
SemilatAlg.mono r step (length (map OK \<tau>s)) A
pres_type step (length (map OK \<tau>s)) A
\<forall>pc<length (map OK \<tau>s). map OK \<tau>s ! pc \<in> A \<and> map OK \<tau>s ! pc \<noteq> Err
bounded step (length (map OK \<tau>s))
OK None \<noteq> Err
wt_step r Err step (map OK \<tau>s)
OK first \<sqsubseteq>\<^bsub>r\<^esub> map OK \<tau>s ! 0
OK first \<in> A
OK first \<noteq> Err
length is = length (map OK \<tau>s)

goal (1 subgoal):
 1. wtl_inst_list is (make_cert step (map OK \<tau>s) (OK None)) f r Err (OK None) step 0 (OK first) \<noteq> Err
[PROOF STEP]
by (rule lbvc.wtl_complete [OF lbvc.intro, OF lbv.intro lbvc_axioms.intro, OF Semilat.intro lbv_axioms.intro])
[PROOF STATE]
proof (state)
this:
wtl_inst_list is (make_cert step (map OK \<tau>s) (OK None)) f r Err (OK None) step 0 (OK first) \<noteq> Err

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wtl_inst_list is (make_cert step (map OK \<tau>s) (OK None)) f r Err (OK None) step 0 (OK first) \<noteq> Err

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
from 0 size
[PROOF STATE]
proof (chain)
picking this:
0 < length is
length is = length (map OK \<tau>s)
[PROOF STEP]
have "\<tau>s \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
0 < length is
length is = length (map OK \<tau>s)

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

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<tau>s \<noteq> []

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
from ck_types
[PROOF STATE]
proof (chain)
picking this:
check_types P mxs mxl (map OK \<tau>s)
[PROOF STEP]
have "check_types P mxs mxl ?cert"
[PROOF STATE]
proof (prove)
using this:
check_types P mxs mxl (map OK \<tau>s)

goal (1 subgoal):
 1. check_types P mxs mxl (make_cert step (map OK \<tau>s) (OK None))
[PROOF STEP]
by (fastforce simp: make_cert_def check_types_def JVM_states_unfold
                  dest!: nth_mem)
[PROOF STATE]
proof (state)
this:
check_types P mxs mxl (make_cert step (map OK \<tau>s) (OK None))

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
check_types P mxs mxl (make_cert step (map OK \<tau>s) (OK None))

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
note 0 size
[PROOF STATE]
proof (state)
this:
0 < length is
length is = length (map OK \<tau>s)

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wtl_inst_list is (make_cert step (map OK \<tau>s) (OK None)) f r Err (OK None) step 0 (OK first) \<noteq> Err
\<tau>s \<noteq> []
check_types P mxs mxl (make_cert step (map OK \<tau>s) (OK None))
0 < length is
length is = length (map OK \<tau>s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wtl_inst_list is (make_cert step (map OK \<tau>s) (OK None)) f r Err (OK None) step 0 (OK first) \<noteq> Err
\<tau>s \<noteq> []
check_types P mxs mxl (make_cert step (map OK \<tau>s) (OK None))
0 < length is
length is = length (map OK \<tau>s)

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
using staticb
[PROOF STATE]
proof (prove)
using this:
wtl_inst_list is (make_cert step (map OK \<tau>s) (OK None)) f r Err (OK None) step 0 (OK first) \<noteq> Err
\<tau>s \<noteq> []
check_types P mxs mxl (make_cert step (map OK \<tau>s) (OK None))
0 < length is
length is = length (map OK \<tau>s)
b = Static \<or> b = NonStatic

goal (1 subgoal):
 1. wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is
[PROOF STEP]
by (simp add: wt_lbv_def lbvjvm_def mk_cert_def step_def_exec [symmetric]
                  check_cert_def make_cert_def nth_append)
[PROOF STATE]
proof (state)
this:
wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem jvm_lbv_correct:
  "wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
let ?\<Phi> = "\<lambda>C mn. let (C,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)) = method P C mn in
              SOME \<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
let ?A = "\<lambda>P C (mn,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,ins,et)). wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert C mn) ins"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
let ?B = "\<lambda>P C (M,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)).
                wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (?\<Phi> C M)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
assume wt: "wt_jvm_prog_lbv P Cert"
[PROOF STATE]
proof (state)
this:
wt_jvm_prog_lbv P Cert

goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wt_jvm_prog_lbv P Cert
[PROOF STEP]
have "wf_prog ?A P"
[PROOF STATE]
proof (prove)
using this:
wt_jvm_prog_lbv P Cert

goal (1 subgoal):
 1. wf_prog (\<lambda>P C (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et). wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert C mn) ins) P
[PROOF STEP]
by(simp add: wt_jvm_prog_lbv_def)
[PROOF STATE]
proof (state)
this:
wf_prog (\<lambda>P C (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et). wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert C mn) ins) P

goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wf_prog (\<lambda>P C (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et). wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert C mn) ins) P

goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
wf_prog (\<lambda>P C (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et). wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert C mn) ins) P

goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
fix wf_md C M b Ts Ca T m bd
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
assume ass1: "wf_prog wf_md P" and sees: "P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca" and
           ass2: "set Ts \<subseteq> types P" and ass3: "bd = (M, b, Ts, T, m)" and
           ass4: "?A P Ca bd"
[PROOF STATE]
proof (state)
this:
wf_prog wf_md P
P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca
set Ts \<subseteq> types P
bd = (M, b, Ts, T, m)
case bd of (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et) \<Rightarrow> wt_lbv P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert Ca mn) ins

goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
from ass3 ass4
[PROOF STATE]
proof (chain)
picking this:
bd = (M, b, Ts, T, m)
case bd of (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et) \<Rightarrow> wt_lbv P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert Ca mn) ins
[PROOF STEP]
have stab: "b = Static \<or> b = NonStatic"
[PROOF STATE]
proof (prove)
using this:
bd = (M, b, Ts, T, m)
case bd of (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et) \<Rightarrow> wt_lbv P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert Ca mn) ins

goal (1 subgoal):
 1. b = Static \<or> b = NonStatic
[PROOF STEP]
by (simp add:wt_lbv_def)
[PROOF STATE]
proof (state)
this:
b = Static \<or> b = NonStatic

goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
from ass1 sees ass2 ass3 ass4
[PROOF STATE]
proof (chain)
picking this:
wf_prog wf_md P
P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca
set Ts \<subseteq> types P
bd = (M, b, Ts, T, m)
case bd of (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et) \<Rightarrow> wt_lbv P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert Ca mn) ins
[PROOF STEP]
have "?B P Ca bd"
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca
set Ts \<subseteq> types P
bd = (M, b, Ts, T, m)
case bd of (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et) \<Rightarrow> wt_lbv P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert Ca mn) ins

goal (1 subgoal):
 1. case bd of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (let (C, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) = method P Ca M in SOME \<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s)
[PROOF STEP]
using sees_method_is_class[OF sees]
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca
set Ts \<subseteq> types P
bd = (M, b, Ts, T, m)
case bd of (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et) \<Rightarrow> wt_lbv P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert Ca mn) ins
is_class P Ca

goal (1 subgoal):
 1. case bd of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (let (C, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) = method P Ca M in SOME \<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s)
[PROOF STEP]
by (auto  dest!: start_context.wt_lbv_wt_method [OF start_context_intro_auxi[OF stab]]
               intro: someI)
[PROOF STATE]
proof (state)
this:
case bd of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (let (C, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) = method P Ca M in SOME \<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s)

goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>wf_prog ?wf_md3 P; P \<turnstile> ?Ca3 sees ?M3, ?b3 :  ?Ts3\<rightarrow>?T3 = ?m3 in ?Ca3; set ?Ts3 \<subseteq> types P; ?bd3 = (?M3, ?b3, ?Ts3, ?T3, ?m3); case ?bd3 of (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et) \<Rightarrow> wt_lbv P ?Ca3 b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert ?Ca3 mn) ins\<rbrakk> \<Longrightarrow> case ?bd3 of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method P ?Ca3 b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (let (C, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) = method P ?Ca3 M in SOME \<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s)

goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wf_prog (\<lambda>P C (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et). wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert C mn) ins) P
\<lbrakk>wf_prog ?wf_md3 P; P \<turnstile> ?Ca3 sees ?M3, ?b3 :  ?Ts3\<rightarrow>?T3 = ?m3 in ?Ca3; set ?Ts3 \<subseteq> types P; ?bd3 = (?M3, ?b3, ?Ts3, ?T3, ?m3); case ?bd3 of (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et) \<Rightarrow> wt_lbv P ?Ca3 b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert ?Ca3 mn) ins\<rbrakk> \<Longrightarrow> case ?bd3 of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method P ?Ca3 b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (let (C, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) = method P ?Ca3 M in SOME \<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s)
[PROOF STEP]
have "wf_prog ?B P"
[PROOF STATE]
proof (prove)
using this:
wf_prog (\<lambda>P C (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et). wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert C mn) ins) P
\<lbrakk>wf_prog ?wf_md3 P; P \<turnstile> ?Ca3 sees ?M3, ?b3 :  ?Ts3\<rightarrow>?T3 = ?m3 in ?Ca3; set ?Ts3 \<subseteq> types P; ?bd3 = (?M3, ?b3, ?Ts3, ?T3, ?m3); case ?bd3 of (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et) \<Rightarrow> wt_lbv P ?Ca3 b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert ?Ca3 mn) ins\<rbrakk> \<Longrightarrow> case ?bd3 of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method P ?Ca3 b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (let (C, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) = method P ?Ca3 M in SOME \<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s)

goal (1 subgoal):
 1. wf_prog (\<lambda>Pa C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (let (C, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) = method P C M in SOME \<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s)) P
[PROOF STEP]
by(rule wf_prog_lift)
[PROOF STATE]
proof (state)
this:
wf_prog (\<lambda>Pa C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (let (C, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) = method P C M in SOME \<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s)) P

goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
hence "wf_jvm_prog\<^bsub>?\<Phi>\<^esub> P"
[PROOF STATE]
proof (prove)
using this:
wf_prog (\<lambda>Pa C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (let (C, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) = method P C M in SOME \<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s)) P

goal (1 subgoal):
 1. wf_jvm_prog\<^bsub>\<lambda>C mn. let (C, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) = method P C mn in SOME \<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s\<^esub> P
[PROOF STEP]
by (simp add: wf_jvm_prog_phi_def)
[PROOF STATE]
proof (state)
this:
wf_jvm_prog\<^bsub>\<lambda>C mn. let (C, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) = method P C mn in SOME \<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s\<^esub> P

goal (1 subgoal):
 1. wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>\<lambda>C mn. let (C, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) = method P C mn in SOME \<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s\<^esub> P

goal (1 subgoal):
 1. wf_jvm_prog P
[PROOF STEP]
by (unfold wf_jvm_prog_def) blast
[PROOF STATE]
proof (state)
this:
wf_jvm_prog P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem jvm_lbv_complete:
  assumes wt: "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P"
  shows "wt_jvm_prog_lbv P (prg_cert P \<Phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
let ?cert = "prg_cert P \<Phi>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
let ?A = "\<lambda>P C (M,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)).
                wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
let ?B = "\<lambda>P C (mn,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,ins,et)).
                wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et (?cert C mn) ins"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
from wt
[PROOF STATE]
proof (chain)
picking this:
wf_jvm_prog\<^bsub>\<Phi>\<^esub> P
[PROOF STEP]
have "wf_prog ?A P"
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>\<Phi>\<^esub> P

goal (1 subgoal):
 1. wf_prog (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P
[PROOF STEP]
by(clarsimp simp: wf_jvm_prog_def wf_jvm_prog_phi_def)
[PROOF STATE]
proof (state)
this:
wf_prog (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P

goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wf_prog (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P

goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
wf_prog (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P

goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
fix wf_md C M b Ts Ca T m bd
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
assume ass1: "wf_prog wf_md P" and sees: "P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca" and
           ass2: "set Ts \<subseteq> types P" and ass3: "bd = (M, b, Ts, T, m)" and
           ass4: "?A P Ca bd"
[PROOF STATE]
proof (state)
this:
wf_prog wf_md P
P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca
set Ts \<subseteq> types P
bd = (M, b, Ts, T, m)
case bd of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> Ca M)

goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
from ass3 ass4
[PROOF STATE]
proof (chain)
picking this:
bd = (M, b, Ts, T, m)
case bd of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> Ca M)
[PROOF STEP]
have stab: "b = Static \<or> b = NonStatic"
[PROOF STATE]
proof (prove)
using this:
bd = (M, b, Ts, T, m)
case bd of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> Ca M)

goal (1 subgoal):
 1. b = Static \<or> b = NonStatic
[PROOF STEP]
by (simp add:wt_method_def)
[PROOF STATE]
proof (state)
this:
b = Static \<or> b = NonStatic

goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
from ass1 sees ass2 ass3 ass4
[PROOF STATE]
proof (chain)
picking this:
wf_prog wf_md P
P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca
set Ts \<subseteq> types P
bd = (M, b, Ts, T, m)
case bd of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> Ca M)
[PROOF STEP]
have "?B P Ca bd"
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca
set Ts \<subseteq> types P
bd = (M, b, Ts, T, m)
case bd of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> Ca M)

goal (1 subgoal):
 1. case bd of (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et) \<Rightarrow> wt_lbv P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 et (prg_cert P \<Phi> Ca mn) ins
[PROOF STEP]
using sees_method_is_class[OF sees]
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca
set Ts \<subseteq> types P
bd = (M, b, Ts, T, m)
case bd of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> Ca M)
is_class P Ca

goal (1 subgoal):
 1. case bd of (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et) \<Rightarrow> wt_lbv P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 et (prg_cert P \<Phi> Ca mn) ins
[PROOF STEP]
by (auto simp add: prg_cert_def
               intro!: start_context.wt_method_wt_lbv start_context_intro_auxi[OF stab])
[PROOF STATE]
proof (state)
this:
case bd of (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et) \<Rightarrow> wt_lbv P Ca b Ts T\<^sub>r mxs mxl\<^sub>0 et (prg_cert P \<Phi> Ca mn) ins

goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>wf_prog ?wf_md3 P; P \<turnstile> ?Ca3 sees ?M3, ?b3 :  ?Ts3\<rightarrow>?T3 = ?m3 in ?Ca3; set ?Ts3 \<subseteq> types P; ?bd3 = (?M3, ?b3, ?Ts3, ?T3, ?m3); case ?bd3 of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method P ?Ca3 b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> ?Ca3 M)\<rbrakk> \<Longrightarrow> case ?bd3 of (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et) \<Rightarrow> wt_lbv P ?Ca3 b Ts T\<^sub>r mxs mxl\<^sub>0 et (prg_cert P \<Phi> ?Ca3 mn) ins

goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wf_prog (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P
\<lbrakk>wf_prog ?wf_md3 P; P \<turnstile> ?Ca3 sees ?M3, ?b3 :  ?Ts3\<rightarrow>?T3 = ?m3 in ?Ca3; set ?Ts3 \<subseteq> types P; ?bd3 = (?M3, ?b3, ?Ts3, ?T3, ?m3); case ?bd3 of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method P ?Ca3 b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> ?Ca3 M)\<rbrakk> \<Longrightarrow> case ?bd3 of (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et) \<Rightarrow> wt_lbv P ?Ca3 b Ts T\<^sub>r mxs mxl\<^sub>0 et (prg_cert P \<Phi> ?Ca3 mn) ins
[PROOF STEP]
have "wf_prog ?B P"
[PROOF STATE]
proof (prove)
using this:
wf_prog (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P
\<lbrakk>wf_prog ?wf_md3 P; P \<turnstile> ?Ca3 sees ?M3, ?b3 :  ?Ts3\<rightarrow>?T3 = ?m3 in ?Ca3; set ?Ts3 \<subseteq> types P; ?bd3 = (?M3, ?b3, ?Ts3, ?T3, ?m3); case ?bd3 of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method P ?Ca3 b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> ?Ca3 M)\<rbrakk> \<Longrightarrow> case ?bd3 of (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et) \<Rightarrow> wt_lbv P ?Ca3 b Ts T\<^sub>r mxs mxl\<^sub>0 et (prg_cert P \<Phi> ?Ca3 mn) ins

goal (1 subgoal):
 1. wf_prog (\<lambda>Pa C (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et). wt_lbv Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 et (prg_cert P \<Phi> C mn) ins) P
[PROOF STEP]
by(rule wf_prog_lift)
[PROOF STATE]
proof (state)
this:
wf_prog (\<lambda>Pa C (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et). wt_lbv Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 et (prg_cert P \<Phi> C mn) ins) P

goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
thus "wt_jvm_prog_lbv P (prg_cert P \<Phi>)"
[PROOF STATE]
proof (prove)
using this:
wf_prog (\<lambda>Pa C (mn, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, ins, et). wt_lbv Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 et (prg_cert P \<Phi> C mn) ins) P

goal (1 subgoal):
 1. wt_jvm_prog_lbv P (prg_cert P \<Phi>)
[PROOF STEP]
by (simp add: wt_jvm_prog_lbv_def)
[PROOF STATE]
proof (state)
this:
wt_jvm_prog_lbv P (prg_cert P \<Phi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_add_K_right: "a \<le>\<^sub>\<K> a + b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> a + b
[PROOF STEP]
unfolding leq_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + (a + b) = a + b
[PROOF STEP]
by (simp add:  add_assoc[symmetric])


[STATEMENT]
lemma par_comm: "a * b = b * a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * b = b * a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a * b = b * a
[PROOF STEP]
have "(b*a) ; (1*1) \<le>\<^sub>\<K> (a;1) * (b;1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b * a ; ((1::'a) * (1::'a)) \<le> a ; (1::'a) * (b ; (1::'a))
[PROOF STEP]
by (simp only:  exchange)
[PROOF STATE]
proof (state)
this:
b * a ; ((1::'a) * (1::'a)) \<le> a ; (1::'a) * (b ; (1::'a))

goal (1 subgoal):
 1. a * b = b * a
[PROOF STEP]
hence "b * a \<le>\<^sub>\<K> a * b"
[PROOF STATE]
proof (prove)
using this:
b * a ; ((1::'a) * (1::'a)) \<le> a ; (1::'a) * (b ; (1::'a))

goal (1 subgoal):
 1. b * a \<le> a * b
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
b * a \<le> a * b

goal (1 subgoal):
 1. a * b = b * a
[PROOF STEP]
hence "a * b \<le>\<^sub>\<K> b * a \<longleftrightarrow> a * b  = b * a"
[PROOF STATE]
proof (prove)
using this:
b * a \<le> a * b

goal (1 subgoal):
 1. (a * b \<le> b * a) = (a * b = b * a)
[PROOF STEP]
by (rule antisym_conv)
[PROOF STATE]
proof (state)
this:
(a * b \<le> b * a) = (a * b = b * a)

goal (1 subgoal):
 1. a * b = b * a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(a * b \<le> b * a) = (a * b = b * a)

goal (1 subgoal):
 1. a * b = b * a
[PROOF STEP]
have "a * b \<le>\<^sub>\<K> b * a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * b \<le> b * a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a * b \<le> b * a
[PROOF STEP]
have "(a*b) ; (1*1) \<le>\<^sub>\<K> (b;1) * (a;1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * b ; ((1::'a) * (1::'a)) \<le> b ; (1::'a) * (a ; (1::'a))
[PROOF STEP]
by (rule  exchange)
[PROOF STATE]
proof (state)
this:
a * b ; ((1::'a) * (1::'a)) \<le> b ; (1::'a) * (a ; (1::'a))

goal (1 subgoal):
 1. a * b \<le> b * a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a * b ; ((1::'a) * (1::'a)) \<le> b ; (1::'a) * (a ; (1::'a))

goal (1 subgoal):
 1. a * b \<le> b * a
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
a * b \<le> b * a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a * b \<le> b * a

goal (1 subgoal):
 1. a * b = b * a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(a * b \<le> b * a) = (a * b = b * a)
a * b \<le> b * a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(a * b \<le> b * a) = (a * b = b * a)
a * b \<le> b * a

goal (1 subgoal):
 1. a * b = b * a
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
a * b = b * a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exchange_2: "(a*b) ; (c*d) \<le>\<^sub>\<K> (a;c) * (b;d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * b ; (c * d) \<le> a ; c * (b ; d)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a * b ; (c * d) \<le> a ; c * (b ; d)
[PROOF STEP]
have "(b*a) ; (c*d) \<le>\<^sub>\<K> (a;c) * (b;d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b * a ; (c * d) \<le> a ; c * (b ; d)
[PROOF STEP]
by (rule exchange)
[PROOF STATE]
proof (state)
this:
b * a ; (c * d) \<le> a ; c * (b ; d)

goal (1 subgoal):
 1. a * b ; (c * d) \<le> a ; c * (b ; d)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
b * a ; (c * d) \<le> a ; c * (b ; d)

goal (1 subgoal):
 1. a * b ; (c * d) \<le> a ; c * (b ; d)
[PROOF STEP]
by (simp add: par_comm)
[PROOF STATE]
proof (state)
this:
a * b ; (c * d) \<le> a ; c * (b ; d)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma seq_inf_par: "a ; b \<le>\<^sub>\<K> a * b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ; b \<le> a * b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a ; b \<le> a * b
[PROOF STEP]
have "(1*a) ; (1*b) \<le>\<^sub>\<K> (a;1) * (1;b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) * a ; ((1::'a) * b) \<le> a ; (1::'a) * ((1::'a) ; b)
[PROOF STEP]
by (rule exchange)
[PROOF STATE]
proof (state)
this:
(1::'a) * a ; ((1::'a) * b) \<le> a ; (1::'a) * ((1::'a) ; b)

goal (1 subgoal):
 1. a ; b \<le> a * b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(1::'a) * a ; ((1::'a) * b) \<le> a ; (1::'a) * ((1::'a) ; b)

goal (1 subgoal):
 1. a ; b \<le> a * b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a ; b \<le> a * b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_seq_inf_par: "a;b + b;a \<le>\<^sub>\<K> a*b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ; b + b ; a \<le> a * b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a ; b + b ; a \<le> a * b
[PROOF STEP]
have "a;b \<le>\<^sub>\<K> a*b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ; b \<le> a * b
[PROOF STEP]
by (rule seq_inf_par)
[PROOF STATE]
proof (state)
this:
a ; b \<le> a * b

goal (1 subgoal):
 1. a ; b + b ; a \<le> a * b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a ; b \<le> a * b

goal (1 subgoal):
 1. a ; b + b ; a \<le> a * b
[PROOF STEP]
have "b;a \<le>\<^sub>\<K> b*a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b ; a \<le> b * a
[PROOF STEP]
by (rule seq_inf_par)
[PROOF STATE]
proof (state)
this:
b ; a \<le> b * a

goal (1 subgoal):
 1. a ; b + b ; a \<le> a * b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a ; b \<le> a * b
b ; a \<le> b * a
[PROOF STEP]
have "a;b + b;a \<le>\<^sub>\<K> a*b + b*a"
[PROOF STATE]
proof (prove)
using this:
a ; b \<le> a * b
b ; a \<le> b * a

goal (1 subgoal):
 1. a ; b + b ; a \<le> a * b + b * a
[PROOF STEP]
by (simp add: add_mono)
[PROOF STATE]
proof (state)
this:
a ; b + b ; a \<le> a * b + b * a

goal (1 subgoal):
 1. a ; b + b ; a \<le> a * b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a ; b + b ; a \<le> a * b + b * a

goal (1 subgoal):
 1. a ; b + b ; a \<le> a * b
[PROOF STEP]
by (simp add: par_comm)
[PROOF STATE]
proof (state)
this:
a ; b + b ; a \<le> a * b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exchange_3: "(a*b) ; c \<le>\<^sub>\<K> a * (b;c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * b ; c \<le> a * (b ; c)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a * b ; c \<le> a * (b ; c)
[PROOF STEP]
have "(a*b) ; (1*c) \<le>\<^sub>\<K> (a;1) * (b;c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * b ; ((1::'a) * c) \<le> a ; (1::'a) * (b ; c)
[PROOF STEP]
by (rule exchange_2)
[PROOF STATE]
proof (state)
this:
a * b ; ((1::'a) * c) \<le> a ; (1::'a) * (b ; c)

goal (1 subgoal):
 1. a * b ; c \<le> a * (b ; c)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a * b ; ((1::'a) * c) \<le> a ; (1::'a) * (b ; c)

goal (1 subgoal):
 1. a * b ; c \<le> a * (b ; c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a * b ; c \<le> a * (b ; c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exchange_4: "a ; (b*c) \<le>\<^sub>\<K> (a;b) * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ; (b * c) \<le> a ; b * c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a ; (b * c) \<le> a ; b * c
[PROOF STEP]
have "(1*a) ; (b*c) \<le>\<^sub>\<K> (a;b) * (1;c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) * a ; (b * c) \<le> a ; b * ((1::'a) ; c)
[PROOF STEP]
by (rule exchange)
[PROOF STATE]
proof (state)
this:
(1::'a) * a ; (b * c) \<le> a ; b * ((1::'a) ; c)

goal (1 subgoal):
 1. a ; (b * c) \<le> a ; b * c
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(1::'a) * a ; (b * c) \<le> a ; b * ((1::'a) ; c)

goal (1 subgoal):
 1. a ; (b * c) \<le> a ; b * c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a ; (b * c) \<le> a ; b * c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma seqstar_inf_parstar: "a\<^sup>; \<le>\<^sub>\<K> a\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a\<^sup>; \<le> a\<^sup>*
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a\<^sup>; \<le> a\<^sup>*
[PROOF STEP]
have "a ; a\<^sup>* \<le>\<^sub>\<K> a * a\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ; a\<^sup>* \<le> a * a\<^sup>*
[PROOF STEP]
by (rule seq_inf_par)
[PROOF STATE]
proof (state)
this:
a ; a\<^sup>* \<le> a * a\<^sup>*

goal (1 subgoal):
 1. a\<^sup>; \<le> a\<^sup>*
[PROOF STEP]
hence "1 + a ; a\<^sup>* \<le>\<^sub>\<K> 1 + a * a\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
a ; a\<^sup>* \<le> a * a\<^sup>*

goal (1 subgoal):
 1. (1::'a) + a ; a\<^sup>* \<le> (1::'a) + a * a\<^sup>*
[PROOF STEP]
by (simp add: add_left_mono)
[PROOF STATE]
proof (state)
this:
(1::'a) + a ; a\<^sup>* \<le> (1::'a) + a * a\<^sup>*

goal (1 subgoal):
 1. a\<^sup>; \<le> a\<^sup>*
[PROOF STEP]
hence "1 + a ; a\<^sup>* \<le>\<^sub>\<K> a\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(1::'a) + a ; a\<^sup>* \<le> (1::'a) + a * a\<^sup>*

goal (1 subgoal):
 1. (1::'a) + a ; a\<^sup>* \<le> a\<^sup>*
[PROOF STEP]
by (simp add: star_unfoldl order_trans)
[PROOF STATE]
proof (state)
this:
(1::'a) + a ; a\<^sup>* \<le> a\<^sup>*

goal (1 subgoal):
 1. a\<^sup>; \<le> a\<^sup>*
[PROOF STEP]
hence "a\<^sup>; ; 1 \<le>\<^sub>\<K> a\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(1::'a) + a ; a\<^sup>* \<le> a\<^sup>*

goal (1 subgoal):
 1. a\<^sup>; ; (1::'a) \<le> a\<^sup>*
[PROOF STEP]
by (rule seqstar_inductl)
[PROOF STATE]
proof (state)
this:
a\<^sup>; ; (1::'a) \<le> a\<^sup>*

goal (1 subgoal):
 1. a\<^sup>; \<le> a\<^sup>*
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a\<^sup>; ; (1::'a) \<le> a\<^sup>*

goal (1 subgoal):
 1. a\<^sup>; \<le> a\<^sup>*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a\<^sup>; \<le> a\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mono_prover_monoI[refine_mono]:
  "monotone (fun_ord (\<le>)) (fun_ord (\<le>)) B \<Longrightarrow> mono B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone (fun_ord (\<le>)) (fun_ord (\<le>)) B \<Longrightarrow> mono B
[PROOF STEP]
apply (simp add: le_fun_def[abs_def] fun_ord_def[abs_def])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma WHILEI_body_trimono: "trimono (WHILEI_body bind return I b f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trimono (WHILEI_body bind return I b f)
[PROOF STEP]
unfolding WHILEI_body_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trimono (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top)
[PROOF STEP]
by refine_mono


[STATEMENT]
lemma WHILEI_unfold: "WHILEI I b f x = (
  if (I x) then (if b x then bind (f x) (WHILEI I b f) else return x) else top) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILEI I b f x = (if I x then if b x then bind (f x) (WHILEI I b f) else return x else top)
[PROOF STEP]
unfolding WHILEI_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. REC (WHILEI_body bind return I b f) x = (if I x then if b x then bind (f x) (REC (WHILEI_body bind return I b f)) else return x else top)
[PROOF STEP]
apply (subst REC_unfold[OF WHILEI_body_trimono])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILEI_body bind return I b f (REC (WHILEI_body bind return I b f)) x = (if I x then if b x then bind (f x) (REC (WHILEI_body bind return I b f)) else return x else top)
[PROOF STEP]
unfolding WHILEI_body_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if I x then if b x then bind (f x) (REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top)) else return x else top) = (if I x then if b x then bind (f x) (REC (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top)) else return x else top)
[PROOF STEP]
apply (rule refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma REC_mono_ref[refine_mono]:
  "\<lbrakk>trimono B; \<And>D x. B D x \<le> B' D x\<rbrakk> \<Longrightarrow> REC B x \<le> REC B' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trimono B; \<And>D x. B D x \<le> B' D x\<rbrakk> \<Longrightarrow> REC B x \<le> REC B' x
[PROOF STEP]
unfolding REC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trimono B; \<And>D x. B D x \<le> B' D x\<rbrakk> \<Longrightarrow> (if trimono B then lfp B x else top) \<le> (if trimono B' then lfp B' x else top)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trimono B; \<And>D x. B D x \<le> B' D x; trimono B'\<rbrakk> \<Longrightarrow> lfp B x \<le> lfp B' x
[PROOF STEP]
apply (rule lfp_mono[THEN le_funD])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Z. \<lbrakk>trimono B; \<And>D x. B D x \<le> B' D x; trimono B'\<rbrakk> \<Longrightarrow> B Z \<le> B' Z
[PROOF STEP]
by (rule le_funI)


[STATEMENT]
lemma RECT_mono_ref[refine_mono]:
  "\<lbrakk>trimono B; \<And>D x. B D x \<le> B' D x\<rbrakk> \<Longrightarrow> RECT B x \<le> RECT B' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trimono B; \<And>D x. B D x \<le> B' D x\<rbrakk> \<Longrightarrow> REC\<^sub>T B x \<le> REC\<^sub>T B' x
[PROOF STEP]
unfolding RECT_gfp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trimono B; \<And>D x. B D x \<le> B' D x\<rbrakk> \<Longrightarrow> (if trimono B then gfp B x else top) \<le> (if trimono B' then gfp B' x else top)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trimono B; \<And>D x. B D x \<le> B' D x; trimono B'\<rbrakk> \<Longrightarrow> gfp B x \<le> gfp B' x
[PROOF STEP]
apply (rule gfp_mono[THEN le_funD])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Z. \<lbrakk>trimono B; \<And>D x. B D x \<le> B' D x; trimono B'\<rbrakk> \<Longrightarrow> B Z \<le> B' Z
[PROOF STEP]
by (rule le_funI)


[STATEMENT]
lemma WHILEIT_unfold: "WHILEIT I b f x = (
  if (I x) then
    (if b x then bind (f x) (WHILEIT I b f) else return x)
  else top) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILEIT I b f x = (if I x then if b x then bind (f x) (WHILEIT I b f) else return x else top)
[PROOF STEP]
unfolding WHILEIT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. REC\<^sub>T (WHILEI_body bind return I b f) x = (if I x then if b x then bind (f x) (REC\<^sub>T (WHILEI_body bind return I b f)) else return x else top)
[PROOF STEP]
apply (subst RECT_unfold[OF WHILEI_body_trimono])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILEI_body bind return I b f (REC\<^sub>T (WHILEI_body bind return I b f)) x = (if I x then if b x then bind (f x) (REC\<^sub>T (WHILEI_body bind return I b f)) else return x else top)
[PROOF STEP]
unfolding WHILEI_body_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if I x then if b x then bind (f x) (REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top)) else return x else top) = (if I x then if b x then bind (f x) (REC\<^sub>T (\<lambda>W s. if I s then if b s then bind (f s) W else return s else top)) else return x else top)
[PROOF STEP]
apply (rule refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma WHILEIT_weaken:
  assumes IW: "\<And>x. I x \<Longrightarrow> I' x"
  shows "WHILEIT I' b f x \<le> WHILEIT I b f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILEIT I' b f x \<le> WHILEIT I b f x
[PROOF STEP]
unfolding WHILEIT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. REC\<^sub>T (WHILEI_body bind return I' b f) x \<le> REC\<^sub>T (WHILEI_body bind return I b f) x
[PROOF STEP]
apply (rule RECT_mono_ref[OF WHILEI_body_trimono])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>D x. WHILEI_body bind return I' b f D x \<le> WHILEI_body bind return I b f D x
[PROOF STEP]
apply (auto simp add: WHILEI_body_def dest: IW)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma WHILEI_le_WHILEIT: "WHILEI I b f s \<le> WHILEIT I b f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILEI I b f s \<le> WHILEIT I b f s
[PROOF STEP]
unfolding WHILEI_def WHILEIT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. REC (WHILEI_body bind return I b f) s \<le> REC\<^sub>T (WHILEI_body bind return I b f) s
[PROOF STEP]
by (rule REC_le_RECT)


[STATEMENT]
lemma WHILE_unfold:
  "WHILE b f s = (if b s then bind (f s) (WHILE b f) else return s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILE b f s = (if b s then bind (f s) (WHILE b f) else return s)
[PROOF STEP]
unfolding WHILE_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILEI (\<lambda>_. True) b f s = (if b s then bind (f s) (WHILEI (\<lambda>_. True) b f) else return s)
[PROOF STEP]
apply (subst WHILEI_unfold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if True then if b s then bind (f s) (WHILEI (\<lambda>_. True) b f) else return s else top) = (if b s then bind (f s) (WHILEI (\<lambda>_. True) b f) else return s)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done