[STATEMENT]
theorem insert_corr:
  assumes "invar_vebt t n " and "x < 2^n "
  shows " set_vebt' t \<union> {x} = set_vebt' (vebt_insert t x) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_vebt' t \<union> {x} = set_vebt' (vebt_insert t x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set_vebt' t \<union> {x} \<subseteq> set_vebt' (vebt_insert t x)
 2. set_vebt' (vebt_insert t x) \<subseteq> set_vebt' t \<union> {x}
[PROOF STEP]
show "set_vebt' t \<union> {x} \<subseteq> set_vebt' (vebt_insert t x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_vebt' t \<union> {x} \<subseteq> set_vebt' (vebt_insert t x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> set_vebt' t \<union> {x} \<Longrightarrow> xa \<in> set_vebt' (vebt_insert t x)
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> set_vebt' t \<union> {x} \<Longrightarrow> xa \<in> set_vebt' (vebt_insert t x)
[PROOF STEP]
assume "y \<in> set_vebt' t \<union> {x}"
[PROOF STATE]
proof (state)
this:
y \<in> set_vebt' t \<union> {x}

goal (1 subgoal):
 1. \<And>xa. xa \<in> set_vebt' t \<union> {x} \<Longrightarrow> xa \<in> set_vebt' (vebt_insert t x)
[PROOF STEP]
show "y \<in>set_vebt' (vebt_insert t x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> set_vebt' (vebt_insert t x)
[PROOF STEP]
proof(cases "x=y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> y \<in> set_vebt' (vebt_insert t x)
 2. x \<noteq> y \<Longrightarrow> y \<in> set_vebt' (vebt_insert t x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> y \<in> set_vebt' (vebt_insert t x)
 2. x \<noteq> y \<Longrightarrow> y \<in> set_vebt' (vebt_insert t x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. y \<in> set_vebt' (vebt_insert t x)
[PROOF STEP]
by (metis (full_types) assms(1) assms(2) both_member_options_equiv_member mem_Collect_eq set_vebt'_def valid_insert_both_member_options_add valid_pres_insert)
[PROOF STATE]
proof (state)
this:
y \<in> set_vebt' (vebt_insert t x)

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> y \<in> set_vebt' (vebt_insert t x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> y \<in> set_vebt' (vebt_insert t x)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> y \<in> set_vebt' (vebt_insert t x)
[PROOF STEP]
have "vebt_member t y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_member t y
[PROOF STEP]
using False \<open>y \<in> set_vebt' t \<union> {x}\<close> set_vebt'_def
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
y \<in> set_vebt' t \<union> {x}
set_vebt' ?t = {x. vebt_member ?t x}

goal (1 subgoal):
 1. vebt_member t y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vebt_member t y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> y \<in> set_vebt' (vebt_insert t x)
[PROOF STEP]
hence "vebt_member (vebt_insert t x) y"
[PROOF STATE]
proof (prove)
using this:
vebt_member t y

goal (1 subgoal):
 1. vebt_member (vebt_insert t x) y
[PROOF STEP]
by (meson assms(1) assms(2) both_member_options_equiv_member member_bound valid_insert_both_member_options_pres valid_pres_insert)
[PROOF STATE]
proof (state)
this:
vebt_member (vebt_insert t x) y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> y \<in> set_vebt' (vebt_insert t x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vebt_member (vebt_insert t x) y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vebt_member (vebt_insert t x) y

goal (1 subgoal):
 1. y \<in> set_vebt' (vebt_insert t x)
[PROOF STEP]
by (simp add: set_vebt'_def)
[PROOF STATE]
proof (state)
this:
y \<in> set_vebt' (vebt_insert t x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y \<in> set_vebt' (vebt_insert t x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set_vebt' t \<union> {x} \<subseteq> set_vebt' (vebt_insert t x)

goal (1 subgoal):
 1. set_vebt' (vebt_insert t x) \<subseteq> set_vebt' t \<union> {x}
[PROOF STEP]
show " set_vebt' (vebt_insert t x) \<subseteq> set_vebt' t \<union> {x} "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_vebt' (vebt_insert t x) \<subseteq> set_vebt' t \<union> {x}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> set_vebt' (vebt_insert t x) \<Longrightarrow> xa \<in> set_vebt' t \<union> {x}
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> set_vebt' (vebt_insert t x) \<Longrightarrow> xa \<in> set_vebt' t \<union> {x}
[PROOF STEP]
assume "y \<in> set_vebt' (vebt_insert t x)"
[PROOF STATE]
proof (state)
this:
y \<in> set_vebt' (vebt_insert t x)

goal (1 subgoal):
 1. \<And>xa. xa \<in> set_vebt' (vebt_insert t x) \<Longrightarrow> xa \<in> set_vebt' t \<union> {x}
[PROOF STEP]
show "y \<in>set_vebt' t \<union> {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> set_vebt' t \<union> {x}
[PROOF STEP]
proof(cases "x=y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> y \<in> set_vebt' t \<union> {x}
 2. x \<noteq> y \<Longrightarrow> y \<in> set_vebt' t \<union> {x}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> y \<in> set_vebt' t \<union> {x}
 2. x \<noteq> y \<Longrightarrow> y \<in> set_vebt' t \<union> {x}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. y \<in> set_vebt' t \<union> {x}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<in> set_vebt' t \<union> {x}

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> y \<in> set_vebt' t \<union> {x}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> y \<in> set_vebt' t \<union> {x}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> y \<in> set_vebt' t \<union> {x}
[PROOF STEP]
hence "vebt_member t y \<or> x=y"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y

goal (1 subgoal):
 1. vebt_member t y \<or> x = y
[PROOF STEP]
using post_member_pre_member
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
\<lbrakk>invar_vebt ?t ?n; ?x < 2 ^ ?n; ?y < 2 ^ ?n; vebt_member (vebt_insert ?t ?x) ?y\<rbrakk> \<Longrightarrow> vebt_member ?t ?y \<or> ?x = ?y

goal (1 subgoal):
 1. vebt_member t y \<or> x = y
[PROOF STEP]
using \<open>y \<in> set_vebt' (vebt_insert t x)\<close> assms(1) assms(2) set_vebt'_def member_bound valid_pres_insert
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
\<lbrakk>invar_vebt ?t ?n; ?x < 2 ^ ?n; ?y < 2 ^ ?n; vebt_member (vebt_insert ?t ?x) ?y\<rbrakk> \<Longrightarrow> vebt_member ?t ?y \<or> ?x = ?y
y \<in> set_vebt' (vebt_insert t x)
invar_vebt t n
x < 2 ^ n
set_vebt' ?t = {x. vebt_member ?t x}
\<lbrakk>vebt_member ?tree ?x; invar_vebt ?tree ?n\<rbrakk> \<Longrightarrow> ?x < 2 ^ ?n
\<lbrakk>invar_vebt ?t ?n; ?x < 2 ^ ?n\<rbrakk> \<Longrightarrow> invar_vebt (vebt_insert ?t ?x) ?n

goal (1 subgoal):
 1. vebt_member t y \<or> x = y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
vebt_member t y \<or> x = y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> y \<in> set_vebt' t \<union> {x}
[PROOF STEP]
hence "vebt_member t y"
[PROOF STATE]
proof (prove)
using this:
vebt_member t y \<or> x = y

goal (1 subgoal):
 1. vebt_member t y
[PROOF STEP]
by (simp add: False)
[PROOF STATE]
proof (state)
this:
vebt_member t y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> y \<in> set_vebt' t \<union> {x}
[PROOF STEP]
hence "y \<in> set_vebt' t"
[PROOF STATE]
proof (prove)
using this:
vebt_member t y

goal (1 subgoal):
 1. y \<in> set_vebt' t
[PROOF STEP]
by (simp add: set_vebt'_def)
[PROOF STATE]
proof (state)
this:
y \<in> set_vebt' t

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> y \<in> set_vebt' t \<union> {x}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> set_vebt' t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<in> set_vebt' t

goal (1 subgoal):
 1. y \<in> set_vebt' t \<union> {x}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<in> set_vebt' t \<union> {x}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y \<in> set_vebt' t \<union> {x}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set_vebt' (vebt_insert t x) \<subseteq> set_vebt' t \<union> {x}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem insert'_pres_valid: assumes "invar_vebt t n" shows "invar_vebt (insert' t x) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar_vebt (insert' t x) n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
invar_vebt t n

goal (1 subgoal):
 1. invar_vebt (insert' t x) n
[PROOF STEP]
apply cases
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>t = Leaf a b; n = Suc 0\<rbrakk> \<Longrightarrow> invar_vebt (insert' t x) n
 2. \<And>treeList na summary m. \<lbrakk>t = Node None n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; n = na + m; \<not> Ex (both_member_options summary); \<forall>t\<in>set treeList. \<not> Ex (both_member_options t)\<rbrakk> \<Longrightarrow> invar_vebt (insert' t x) n
 3. \<And>treeList na summary m. \<lbrakk>t = Node None n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; n = na + m; \<not> Ex (both_member_options summary); \<forall>t\<in>set treeList. \<not> Ex (both_member_options t)\<rbrakk> \<Longrightarrow> invar_vebt (insert' t x) n
 4. \<And>treeList na summary m mi ma. \<lbrakk>t = Node (Some (mi, ma)) n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; n = na + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); mi \<le> ma; ma < 2 ^ n; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> invar_vebt (insert' t x) n
 5. \<And>treeList na summary m mi ma. \<lbrakk>t = Node (Some (mi, ma)) n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; n = na + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); mi \<le> ma; ma < 2 ^ n; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> invar_vebt (insert' t x) n
[PROOF STEP]
apply (metis One_nat_def deg1Leaf insert'.simps(1) vebt_insert.simps(1))
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>treeList na summary m. \<lbrakk>t = Node None n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; n = na + m; \<not> Ex (both_member_options summary); \<forall>t\<in>set treeList. \<not> Ex (both_member_options t)\<rbrakk> \<Longrightarrow> invar_vebt (insert' t x) n
 2. \<And>treeList na summary m. \<lbrakk>t = Node None n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; n = na + m; \<not> Ex (both_member_options summary); \<forall>t\<in>set treeList. \<not> Ex (both_member_options t)\<rbrakk> \<Longrightarrow> invar_vebt (insert' t x) n
 3. \<And>treeList na summary m mi ma. \<lbrakk>t = Node (Some (mi, ma)) n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; n = na + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); mi \<le> ma; ma < 2 ^ n; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> invar_vebt (insert' t x) n
 4. \<And>treeList na summary m mi ma. \<lbrakk>t = Node (Some (mi, ma)) n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; n = na + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); mi \<le> ma; ma < 2 ^ n; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> invar_vebt (insert' t x) n
[PROOF STEP]
apply (metis assms insert'.simps(2) leI valid_pres_insert)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem insert'_correct: assumes "invar_vebt t n"
  shows "set_vebt (insert' t x) = (set_vebt t \<union> {x})\<inter>{0..2^n-1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
proof(cases t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14. t = Node x11 x12 x13 x14 \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
 2. \<And>x21 x22. t = Leaf x21 x22 \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
case (Node x11 x12 x13 x14)
[PROOF STATE]
proof (state)
this:
t = Node x11 x12 x13 x14

goal (2 subgoals):
 1. \<And>x11 x12 x13 x14. t = Node x11 x12 x13 x14 \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
 2. \<And>x21 x22. t = Leaf x21 x22 \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t = Node x11 x12 x13 x14
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Node x11 x12 x13 x14

goal (1 subgoal):
 1. set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
proof(cases "x < 2^n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>t = Node x11 x12 x13 x14; x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
 2. \<lbrakk>t = Node x11 x12 x13 x14; \<not> x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x < 2 ^ n

goal (2 subgoals):
 1. \<lbrakk>t = Node x11 x12 x13 x14; x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
 2. \<lbrakk>t = Node x11 x12 x13 x14; \<not> x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
hence "set_vebt (insert'  t x) = set_vebt(vebt_insert t x)"
[PROOF STATE]
proof (prove)
using this:
x < 2 ^ n

goal (1 subgoal):
 1. set_vebt (insert' t x) = set_vebt (vebt_insert t x)
[PROOF STEP]
by (metis Node assms deg_deg_n insert'.simps(2) leD)
[PROOF STATE]
proof (state)
this:
set_vebt (insert' t x) = set_vebt (vebt_insert t x)

goal (2 subgoals):
 1. \<lbrakk>t = Node x11 x12 x13 x14; x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
 2. \<lbrakk>t = Node x11 x12 x13 x14; \<not> x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set_vebt (insert' t x) = set_vebt (vebt_insert t x)

goal (2 subgoals):
 1. \<lbrakk>t = Node x11 x12 x13 x14; x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
 2. \<lbrakk>t = Node x11 x12 x13 x14; \<not> x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
hence "set_vebt(vebt_insert t x) = set_vebt t \<union> {x}"
[PROOF STATE]
proof (prove)
using this:
set_vebt (insert' t x) = set_vebt (vebt_insert t x)

goal (1 subgoal):
 1. set_vebt (vebt_insert t x) = set_vebt t \<union> {x}
[PROOF STEP]
using True assms insert_correct
[PROOF STATE]
proof (prove)
using this:
set_vebt (insert' t x) = set_vebt (vebt_insert t x)
x < 2 ^ n
invar_vebt t n
\<lbrakk>invar_vebt ?t ?n; ?x < 2 ^ ?n\<rbrakk> \<Longrightarrow> set_vebt ?t \<union> {?x} = set_vebt (vebt_insert ?t ?x)

goal (1 subgoal):
 1. set_vebt (vebt_insert t x) = set_vebt t \<union> {x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_vebt (vebt_insert t x) = set_vebt t \<union> {x}

goal (2 subgoals):
 1. \<lbrakk>t = Node x11 x12 x13 x14; x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
 2. \<lbrakk>t = Node x11 x12 x13 x14; \<not> x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set_vebt (vebt_insert t x) = set_vebt t \<union> {x}

goal (2 subgoals):
 1. \<lbrakk>t = Node x11 x12 x13 x14; x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
 2. \<lbrakk>t = Node x11 x12 x13 x14; \<not> x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
hence "set_vebt t \<union> {x} = (set_vebt t \<union> {x})\<inter>{0..2^n-1} "
[PROOF STATE]
proof (prove)
using this:
set_vebt (vebt_insert t x) = set_vebt t \<union> {x}

goal (1 subgoal):
 1. set_vebt t \<union> {x} = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
by (metis Diff_Diff_Int True assms calculation(1) inf_le1 inrange le_inf_iff order_refl subset_antisym set_vebt'_def set_vebt_def set_vebt_set_vebt'_valid valid_pres_insert)
[PROOF STATE]
proof (state)
this:
set_vebt t \<union> {x} = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}

goal (2 subgoals):
 1. \<lbrakk>t = Node x11 x12 x13 x14; x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
 2. \<lbrakk>t = Node x11 x12 x13 x14; \<not> x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set_vebt (insert' t x) = set_vebt (vebt_insert t x)
set_vebt (vebt_insert t x) = set_vebt t \<union> {x}
set_vebt t \<union> {x} = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set_vebt (insert' t x) = set_vebt (vebt_insert t x)
set_vebt (vebt_insert t x) = set_vebt t \<union> {x}
set_vebt t \<union> {x} = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}

goal (1 subgoal):
 1. set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}

goal (1 subgoal):
 1. \<lbrakk>t = Node x11 x12 x13 x14; \<not> x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>t = Node x11 x12 x13 x14; \<not> x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x < 2 ^ n

goal (1 subgoal):
 1. \<lbrakk>t = Node x11 x12 x13 x14; \<not> x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
hence "set_vebt (insert'  t x) = set_vebt t"
[PROOF STATE]
proof (prove)
using this:
\<not> x < 2 ^ n

goal (1 subgoal):
 1. set_vebt (insert' t x) = set_vebt t
[PROOF STEP]
by (metis Node assms deg_deg_n insert'.simps(2) leI)
[PROOF STATE]
proof (state)
this:
set_vebt (insert' t x) = set_vebt t

goal (1 subgoal):
 1. \<lbrakk>t = Node x11 x12 x13 x14; \<not> x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set_vebt (insert' t x) = set_vebt t

goal (1 subgoal):
 1. \<lbrakk>t = Node x11 x12 x13 x14; \<not> x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
hence "set_vebt t = (set_vebt t \<union> {x})\<inter>{0..2^n-1} "
[PROOF STATE]
proof (prove)
using this:
set_vebt (insert' t x) = set_vebt t

goal (1 subgoal):
 1. set_vebt t = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
by (smt (z3) False Int_commute Int_insert_right_if0 Un_Int_assoc_eq assms atLeastAtMost_iff boolean_algebra_cancel.sup0 inf_bot_right inrange le_add_diff_inverse le_imp_less_Suc one_le_numeral one_le_power plus_1_eq_Suc sup_commute set_vebt_set_vebt'_valid)
[PROOF STATE]
proof (state)
this:
set_vebt t = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}

goal (1 subgoal):
 1. \<lbrakk>t = Node x11 x12 x13 x14; \<not> x < 2 ^ n\<rbrakk> \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set_vebt (insert' t x) = set_vebt t
set_vebt t = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set_vebt (insert' t x) = set_vebt t
set_vebt t = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}

goal (1 subgoal):
 1. set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}

goal (1 subgoal):
 1. \<And>x21 x22. t = Leaf x21 x22 \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. t = Leaf x21 x22 \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
case (Leaf x21 x22)
[PROOF STATE]
proof (state)
this:
t = Leaf x21 x22

goal (1 subgoal):
 1. \<And>x21 x22. t = Leaf x21 x22 \<Longrightarrow> set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t = Leaf x21 x22
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Leaf x21 x22

goal (1 subgoal):
 1. set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}
[PROOF STEP]
apply(auto simp add:  insert'.simps vebt_insert.simps set_vebt_def both_member_options_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>t = Leaf x21 x22; x = Suc 0; \<not> Suc 0 \<le> 2 ^ n - Suc 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>t = Leaf x21 True; x = 0; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>t = Leaf x21 True; x \<noteq> Suc 0; 0 < x; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
invar_vebt t n

goal (4 subgoals):
 1. \<lbrakk>t = Leaf x21 x22; x = Suc 0; \<not> Suc 0 \<le> 2 ^ n - Suc 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>t = Leaf x21 True; x = 0; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>t = Leaf x21 True; x \<noteq> Suc 0; 0 < x; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply cases
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a b. \<lbrakk>t = Leaf x21 x22; x = Suc 0; \<not> Suc 0 \<le> 2 ^ n - Suc 0; t = Leaf a b; n = Suc 0\<rbrakk> \<Longrightarrow> False
 2. \<And>treeList na summary m. \<lbrakk>t = Leaf x21 x22; x = Suc 0; \<not> Suc 0 \<le> 2 ^ n - Suc 0; t = Node None n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; n = na + m; \<not> Ex (both_member_options summary); \<forall>t\<in>set treeList. \<not> Ex (both_member_options t)\<rbrakk> \<Longrightarrow> False
 3. \<And>treeList na summary m. \<lbrakk>t = Leaf x21 x22; x = Suc 0; \<not> Suc 0 \<le> 2 ^ n - Suc 0; t = Node None n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; n = na + m; \<not> Ex (both_member_options summary); \<forall>t\<in>set treeList. \<not> Ex (both_member_options t)\<rbrakk> \<Longrightarrow> False
 4. \<And>treeList na summary m mi ma. \<lbrakk>t = Leaf x21 x22; x = Suc 0; \<not> Suc 0 \<le> 2 ^ n - Suc 0; t = Node (Some (mi, ma)) n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; n = na + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); mi \<le> ma; ma < 2 ^ n; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> False
 5. \<And>treeList na summary m mi ma. \<lbrakk>t = Leaf x21 x22; x = Suc 0; \<not> Suc 0 \<le> 2 ^ n - Suc 0; t = Node (Some (mi, ma)) n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; n = na + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); mi \<le> ma; ma < 2 ^ n; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> False
 6. \<lbrakk>t = Leaf x21 True; x = 0; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0\<rbrakk> \<Longrightarrow> False
 7. \<lbrakk>t = Leaf x21 True; x \<noteq> Suc 0; 0 < x; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0\<rbrakk> \<Longrightarrow> False
 8. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t = Leaf x21 True; x = 0; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>t = Leaf x21 True; x \<noteq> Suc 0; 0 < x; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
invar_vebt t n

goal (3 subgoals):
 1. \<lbrakk>t = Leaf x21 True; x = 0; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>t = Leaf x21 True; x \<noteq> Suc 0; 0 < x; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply cases
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>a b. \<lbrakk>t = Leaf x21 True; x = 0; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0; t = Leaf a b; n = Suc 0\<rbrakk> \<Longrightarrow> False
 2. \<And>treeList na summary m. \<lbrakk>t = Leaf x21 True; x = 0; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0; t = Node None n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; n = na + m; \<not> Ex (both_member_options summary); \<forall>t\<in>set treeList. \<not> Ex (both_member_options t)\<rbrakk> \<Longrightarrow> False
 3. \<And>treeList na summary m. \<lbrakk>t = Leaf x21 True; x = 0; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0; t = Node None n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; n = na + m; \<not> Ex (both_member_options summary); \<forall>t\<in>set treeList. \<not> Ex (both_member_options t)\<rbrakk> \<Longrightarrow> False
 4. \<And>treeList na summary m mi ma. \<lbrakk>t = Leaf x21 True; x = 0; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0; t = Node (Some (mi, ma)) n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; n = na + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); mi \<le> ma; ma < 2 ^ n; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> False
 5. \<And>treeList na summary m mi ma. \<lbrakk>t = Leaf x21 True; x = 0; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0; t = Node (Some (mi, ma)) n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; n = na + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); mi \<le> ma; ma < 2 ^ n; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> False
 6. \<lbrakk>t = Leaf x21 True; x \<noteq> Suc 0; 0 < x; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0\<rbrakk> \<Longrightarrow> False
 7. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t = Leaf x21 True; x \<noteq> Suc 0; 0 < x; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
invar_vebt t n

goal (2 subgoals):
 1. \<lbrakk>t = Leaf x21 True; x \<noteq> Suc 0; 0 < x; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply cases
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>t = Leaf x21 True; x \<noteq> Suc 0; 0 < x; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0; t = Leaf a b; n = Suc 0\<rbrakk> \<Longrightarrow> False
 2. \<And>treeList na summary m. \<lbrakk>t = Leaf x21 True; x \<noteq> Suc 0; 0 < x; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0; t = Node None n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; n = na + m; \<not> Ex (both_member_options summary); \<forall>t\<in>set treeList. \<not> Ex (both_member_options t)\<rbrakk> \<Longrightarrow> False
 3. \<And>treeList na summary m. \<lbrakk>t = Leaf x21 True; x \<noteq> Suc 0; 0 < x; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0; t = Node None n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; n = na + m; \<not> Ex (both_member_options summary); \<forall>t\<in>set treeList. \<not> Ex (both_member_options t)\<rbrakk> \<Longrightarrow> False
 4. \<And>treeList na summary m mi ma. \<lbrakk>t = Leaf x21 True; x \<noteq> Suc 0; 0 < x; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0; t = Node (Some (mi, ma)) n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; n = na + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); mi \<le> ma; ma < 2 ^ n; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> False
 5. \<And>treeList na summary m mi ma. \<lbrakk>t = Leaf x21 True; x \<noteq> Suc 0; 0 < x; x22; \<not> Suc 0 \<le> 2 ^ n - Suc 0; t = Node (Some (mi, ma)) n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; n = na + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); mi \<le> ma; ma < 2 ^ n; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> False
 6. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
invar_vebt t n

goal (1 subgoal):
 1. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply cases
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0; t = Leaf a b; n = Suc 0\<rbrakk> \<Longrightarrow> False
 2. \<And>treeList na summary m. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0; t = Node None n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; n = na + m; \<not> Ex (both_member_options summary); \<forall>t\<in>set treeList. \<not> Ex (both_member_options t)\<rbrakk> \<Longrightarrow> False
 3. \<And>treeList na summary m. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0; t = Node None n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; n = na + m; \<not> Ex (both_member_options summary); \<forall>t\<in>set treeList. \<not> Ex (both_member_options t)\<rbrakk> \<Longrightarrow> False
 4. \<And>treeList na summary m mi ma. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0; t = Node (Some (mi, ma)) n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = na; n = na + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); mi \<le> ma; ma < 2 ^ n; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> False
 5. \<And>treeList na summary m mi ma. \<lbrakk>t = Leaf x21 x22; 0 < x; x \<le> 2 ^ n - Suc 0; x \<noteq> Suc 0; t = Node (Some (mi, ma)) n treeList summary; \<forall>t\<in>set treeList. invar_vebt t na; invar_vebt summary m; length treeList = 2 ^ m; m = Suc na; n = na + m; \<forall>i<2 ^ m. Ex (both_member_options (treeList ! i)) = both_member_options summary i; mi = ma \<longrightarrow> (\<forall>t\<in>set treeList. \<not> Ex (both_member_options t)); mi \<le> ma; ma < 2 ^ n; mi \<noteq> ma \<longrightarrow> (\<forall>i<2 ^ m. (high ma na = i \<longrightarrow> both_member_options (treeList ! i) (low ma na)) \<and> (\<forall>x. high x na = i \<and> both_member_options (treeList ! i) (low x na) \<longrightarrow> mi < x \<and> x \<le> ma))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
set_vebt (insert' t x) = (set_vebt t \<union> {x}) \<inter> {0..2 ^ n - 1}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma do_app_no_runtime_error:
  assumes "do_app (refs s, ffi s) op0 (rev vs) = Some ((refs', ffi'), res)"
  shows "res \<noteq> Rerr (Rabort Rtimeout_error)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. res \<noteq> Rerr (Rabort Rtimeout_error)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
do_app (refs s, ffi s) op0 (rev vs) = Some ((refs', ffi'), res)

goal (1 subgoal):
 1. res \<noteq> Rerr (Rabort Rtimeout_error)
[PROOF STEP]
apply (auto
        split: op0.splits list.splits v.splits lit.splits if_splits word_size.splits
               eq_result.splits option.splits store_v.splits
        simp: store_alloc_def store_assign_def call_FFI_def Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x39 x3 x5 x2a. \<lbrakk>op0 = FFI x39; vs = [Loc x5, Litv (StrLit x3)]; store_lookup x5 (refs s) = Some (W8array x2a); final_event (ffi s) = None; x39 \<noteq> []; (case case oracle0 (ffi s) x39 (ffi_state (ffi s)) (map (\<lambda>c2. word_of_nat (of_char c2)) x3) x2a of Oracle_return ffi' bytes' \<Rightarrow> if length bytes' = length x2a then (update_io_events (\<lambda>_. io_events (ffi s) @ [IO_event x39 (map (\<lambda>c2. word_of_nat (of_char c2)) x3) (zipSameLength x2a bytes')]) (update_ffi_state (\<lambda>_. ffi') (ffi s)), bytes') else (update_final_event (\<lambda>_. Some (Final_event x39 (map (\<lambda>c2. word_of_nat (of_char c2)) x3) x2a FFI_failed)) (ffi s), x2a) | Oracle_diverge \<Rightarrow> (update_final_event (\<lambda>_. Some (Final_event x39 (map (\<lambda>c2. word_of_nat (of_char c2)) x3) x2a FFI_diverged)) (ffi s), x2a) | Oracle_fail \<Rightarrow> (update_final_event (\<lambda>_. Some (Final_event x39 (map (\<lambda>c2. word_of_nat (of_char c2)) x3) x2a FFI_failed)) (ffi s), x2a) of (t', ws') \<Rightarrow> case if x5 < length (refs s) \<and> store_v_same_type (refs s ! x5) (W8array ws') then Some ((refs s)[x5 := W8array ws']) else None of None \<Rightarrow> None | Some s' \<Rightarrow> Some ((s', t'), Rval (Conv None []))) = Some ((refs', ffi'), Rerr (Rabort Rtimeout_error)); res = Rerr (Rabort Rtimeout_error)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (auto split: oracle_result.splits if_splits)


[STATEMENT]
lemma big_unclocked0:
  "evaluate_match ck env s v pes err_v r1 \<Longrightarrow> ck = False \<Longrightarrow> snd r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> (clock s) = (clock (fst r1))"
  "evaluate_list ck env s es r2 \<Longrightarrow> ck = False \<Longrightarrow> snd r2 \<noteq> Rerr (Rabort Rtimeout_error) \<and> (clock s) = (clock (fst r2))"
  "evaluate ck env s e r3 \<Longrightarrow> ck = False \<Longrightarrow> snd r3 \<noteq> Rerr (Rabort Rtimeout_error) \<and> (clock s) = (clock (fst r3))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>evaluate_match ck env s v pes err_v r1; ck = False\<rbrakk> \<Longrightarrow> snd r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock (fst r1)) &&& (\<lbrakk>evaluate_list ck env s es r2; ck = False\<rbrakk> \<Longrightarrow> snd r2 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock (fst r2)) &&& (\<lbrakk>evaluate ck env s e r3; ck = False\<rbrakk> \<Longrightarrow> snd r3 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock (fst r3))
[PROOF STEP]
by (induction rule: evaluate_match_evaluate_list_evaluate.inducts)
     (auto intro!: do_app_no_runtime_error)


[STATEMENT]
lemma big_unclocked1:
 "evaluate_match ck env s v pes err_v r1 \<Longrightarrow> \<forall>st' r. r1 = (st', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error)
  \<longrightarrow> evaluate_match False env (s \<lparr> clock := cnt \<rparr>) v pes err_v ((st' \<lparr> clock := cnt \<rparr>), r)"
 "evaluate_list ck env s es r2 \<Longrightarrow> \<forall>st' r. r2 = (st', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error)
  \<longrightarrow> evaluate_list False env (s \<lparr> clock := cnt \<rparr>) es ((st' \<lparr> clock := cnt \<rparr>), r)"
 "evaluate ck env s e r3 \<Longrightarrow> \<forall>st' r. r3 = (st', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error)
 \<longrightarrow> evaluate False env (s \<lparr> clock := cnt \<rparr>) e ((st' \<lparr> clock := cnt \<rparr>), r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (evaluate_match ck env s v pes err_v r1 \<Longrightarrow> \<forall>st' r. r1 = (st', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_match False env (update_clock (\<lambda>_. cnt) s) v pes err_v (update_clock (\<lambda>_. cnt) st', r)) &&& (evaluate_list ck env s es r2 \<Longrightarrow> \<forall>st' r. r2 = (st', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate_list False env (update_clock (\<lambda>_. cnt) s) es (update_clock (\<lambda>_. cnt) st', r)) &&& (evaluate ck env s e r3 \<Longrightarrow> \<forall>st' r. r3 = (st', r) \<and> r \<noteq> Rerr (Rabort Rtimeout_error) \<longrightarrow> evaluate False env (update_clock (\<lambda>_. cnt) s) e (update_clock (\<lambda>_. cnt) st', r))
[PROOF STEP]
by (induction arbitrary: cnt and cnt and cnt rule: evaluate_match_evaluate_list_evaluate.inducts)
   (auto intro: evaluate_match_evaluate_list_evaluate.intros split:if_splits)


[STATEMENT]
lemma big_unclocked_ignore:
 "evaluate_match ck env s v pes err_v (st', r1) \<Longrightarrow> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<Longrightarrow>
    evaluate_match False env (s \<lparr> clock := cnt \<rparr>) v pes err_v (st' \<lparr> clock := cnt \<rparr>, r1)"
 "evaluate_list ck env s es (st', r2) \<Longrightarrow> r2 \<noteq> Rerr (Rabort Rtimeout_error) \<Longrightarrow>
    evaluate_list False env (s \<lparr> clock := cnt \<rparr>) es (st' \<lparr> clock := cnt \<rparr>, r2)"
 "evaluate ck env s e (st', r3) \<Longrightarrow> r3 \<noteq> Rerr (Rabort Rtimeout_error) \<Longrightarrow>
    evaluate False env (s \<lparr> clock := cnt \<rparr>) e (st' \<lparr> clock := cnt \<rparr>, r3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>evaluate_match ck env s v pes err_v (st', r1); r1 \<noteq> Rerr (Rabort Rtimeout_error)\<rbrakk> \<Longrightarrow> evaluate_match False env (update_clock (\<lambda>_. cnt) s) v pes err_v (update_clock (\<lambda>_. cnt) st', r1)) &&& (\<lbrakk>evaluate_list ck env s es (st', r2); r2 \<noteq> Rerr (Rabort Rtimeout_error)\<rbrakk> \<Longrightarrow> evaluate_list False env (update_clock (\<lambda>_. cnt) s) es (update_clock (\<lambda>_. cnt) st', r2)) &&& (\<lbrakk>evaluate ck env s e (st', r3); r3 \<noteq> Rerr (Rabort Rtimeout_error)\<rbrakk> \<Longrightarrow> evaluate False env (update_clock (\<lambda>_. cnt) s) e (update_clock (\<lambda>_. cnt) st', r3))
[PROOF STEP]
by (rule big_unclocked1[rule_format]; (assumption | simp))+


[STATEMENT]
lemma big_unclocked:
  assumes "evaluate False env s e (s',r) \<Longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error)"
  assumes "evaluate False env s e (s',r) \<Longrightarrow> clock s = clock s'"
  assumes "evaluate False env (s \<lparr> clock := count1 \<rparr>) e ((s' \<lparr> clock := count1 \<rparr>),r)"
  shows "evaluate False env (s \<lparr> clock := count2 \<rparr>) e ((s' \<lparr> clock := count2 \<rparr>),r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate False env (update_clock (\<lambda>_. count2) s) e (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
using assms big_unclocked0(3) big_unclocked_ignore(3)
[PROOF STATE]
proof (prove)
using this:
evaluate False env s e (s', r) \<Longrightarrow> r \<noteq> Rerr (Rabort Rtimeout_error)
evaluate False env s e (s', r) \<Longrightarrow> clock s = clock s'
evaluate False env (update_clock (\<lambda>_. count1) s) e (update_clock (\<lambda>_. count1) s', r)
\<lbrakk>evaluate ?ck ?env ?s ?e ?r3.0; ?ck = False\<rbrakk> \<Longrightarrow> snd ?r3.0 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock ?s = clock (fst ?r3.0)
\<lbrakk>evaluate ?ck ?env ?s ?e (?st', ?r3.0); ?r3.0 \<noteq> Rerr (Rabort Rtimeout_error)\<rbrakk> \<Longrightarrow> evaluate False ?env (update_clock (\<lambda>_. ?cnt) ?s) ?e (update_clock (\<lambda>_. ?cnt) ?st', ?r3.0)

goal (1 subgoal):
 1. evaluate False env (update_clock (\<lambda>_. count2) s) e (update_clock (\<lambda>_. count2) s', r)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma add_to_counter0:
  "evaluate_match ck env s v pes err_v r1 \<Longrightarrow> \<forall>s' r' extra. (r1 = (s',r')) \<and> (r' \<noteq> Rerr (Rabort Rtimeout_error)) \<and> (ck = True)
   \<longrightarrow> evaluate_match True env (s \<lparr> clock := (clock   s)+extra \<rparr>) v pes err_v ((s' \<lparr> clock := (clock   s')+ extra\<rparr>),r')"
  "evaluate_list ck env s es r2 \<Longrightarrow>  \<forall>s' r' extra. (r2 = (s',r')) \<and> (r' \<noteq> Rerr (Rabort Rtimeout_error)) \<and> (ck = True)
   \<longrightarrow> evaluate_list True env (s \<lparr> clock := (clock   s)+extra \<rparr>) es ((s' \<lparr> clock := (clock   s')+ extra\<rparr>),r')"
  "evaluate ck env s e r3 \<Longrightarrow> \<forall>s' r' extra. (r3 = (s',r')) \<and> (r' \<noteq> Rerr (Rabort Rtimeout_error)) \<and> (ck = True)
   \<longrightarrow> evaluate True env (s \<lparr> clock := (clock   s)+extra \<rparr>) e ((s' \<lparr> clock := (clock   s')+ extra\<rparr>),r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (evaluate_match ck env s v pes err_v r1 \<Longrightarrow> \<forall>s' r' extra. r1 = (s', r') \<and> r' \<noteq> Rerr (Rabort Rtimeout_error) \<and> ck = True \<longrightarrow> evaluate_match True env (update_clock (\<lambda>_. clock s + extra) s) v pes err_v (update_clock (\<lambda>_. clock s' + extra) s', r')) &&& (evaluate_list ck env s es r2 \<Longrightarrow> \<forall>s' r' extra. r2 = (s', r') \<and> r' \<noteq> Rerr (Rabort Rtimeout_error) \<and> ck = True \<longrightarrow> evaluate_list True env (update_clock (\<lambda>_. clock s + extra) s) es (update_clock (\<lambda>_. clock s' + extra) s', r')) &&& (evaluate ck env s e r3 \<Longrightarrow> \<forall>s' r' extra. r3 = (s', r') \<and> r' \<noteq> Rerr (Rabort Rtimeout_error) \<and> ck = True \<longrightarrow> evaluate True env (update_clock (\<lambda>_. clock s + extra) s) e (update_clock (\<lambda>_. clock s' + extra) s', r'))
[PROOF STEP]
by (induction rule: evaluate_match_evaluate_list_evaluate.inducts)
   (auto intro: evaluate_match_evaluate_list_evaluate.intros)


[STATEMENT]
lemma add_clock:
  "evaluate_match ck env s v pes err_v r1 \<Longrightarrow> \<forall>s' r'. (r1 = (s', r') \<and> ck = False
   \<longrightarrow> (\<exists>c. evaluate_match True env (s (| clock := c |)) v pes err_v ((s' (| clock := 0 |)),r')))"
  "evaluate_list ck env s es r2 \<Longrightarrow> \<forall>s' r'. (r2 = (s', r') \<and> ck = False
   \<longrightarrow> (\<exists>c. evaluate_list True env (s (| clock := c |)) es ((s' (| clock := 0 |)),r')))"
  "evaluate ck env s e r3 \<Longrightarrow> \<forall>s' r'. (r3 = (s', r') \<and> ck = False
   \<longrightarrow> (\<exists>c. evaluate True env (s (| clock := c |)) e ((s' (| clock := 0 |)),r')))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (evaluate_match ck env s v pes err_v r1 \<Longrightarrow> \<forall>s' r'. r1 = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_match True env (update_clock (\<lambda>_. c) s) v pes err_v (update_clock (\<lambda>_. 0) s', r'))) &&& (evaluate_list ck env s es r2 \<Longrightarrow> \<forall>s' r'. r2 = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_list True env (update_clock (\<lambda>_. c) s) es (update_clock (\<lambda>_. 0) s', r'))) &&& (evaluate ck env s e r3 \<Longrightarrow> \<forall>s' r'. r3 = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r')))
[PROOF STEP]
proof (induction rule:evaluate_match_evaluate_list_evaluate.inducts)
[PROOF STATE]
proof (state)
goal (42 subgoals):
 1. \<And>ck env l s. \<forall>s' r'. (s, Rval (Litv l)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) (Lit l) (update_clock (\<lambda>_. 0) s', r'))
 2. \<And>ck env e s1 s2 v1. \<lbrakk>evaluate ck s1 env e (s2, Rval v1); \<forall>s' r'. (s2, Rval v1) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) e (update_clock (\<lambda>_. 0) s', r'))\<rbrakk> \<Longrightarrow> \<forall>s' r'. (s2, Rerr (Rraise v1)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) (Raise e) (update_clock (\<lambda>_. 0) s', r'))
 3. \<And>ck env e s1 s2 err. \<lbrakk>evaluate ck s1 env e (s2, Rerr err); \<forall>s' r'. (s2, Rerr err) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) e (update_clock (\<lambda>_. 0) s', r'))\<rbrakk> \<Longrightarrow> \<forall>s' r'. (s2, Rerr err) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) (Raise e) (update_clock (\<lambda>_. 0) s', r'))
 4. \<And>ck s1 s2 env e v1 pes. \<lbrakk>evaluate ck s1 env e (s2, Rval v1); \<forall>s' r'. (s2, Rval v1) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) e (update_clock (\<lambda>_. 0) s', r'))\<rbrakk> \<Longrightarrow> \<forall>s' r'. (s2, Rval v1) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) (Handle e pes) (update_clock (\<lambda>_. 0) s', r'))
 5. \<And>ck s1 s2 env e pes v1 bv. (evaluate ck env s1 e (s2, Rerr (Rraise v1)) \<and> (\<forall>s' r'. (s2, Rerr (Rraise v1)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s1) e (update_clock (\<lambda>_. 0) s', r')))) \<and> evaluate_match ck env s2 v1 pes v1 bv \<and> (\<forall>s' r'. bv = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_match True env (update_clock (\<lambda>_. c) s2) v1 pes v1 (update_clock (\<lambda>_. 0) s', r'))) \<Longrightarrow> \<forall>s' r'. bv = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s1) (Handle e pes) (update_clock (\<lambda>_. 0) s', r'))
 6. \<And>ck s1 s2 env e pes a. \<lbrakk>evaluate ck env s1 e (s2, Rerr (Rabort a)); \<forall>s' r'. (s2, Rerr (Rabort a)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s1) e (update_clock (\<lambda>_. 0) s', r'))\<rbrakk> \<Longrightarrow> \<forall>s' r'. (s2, Rerr (Rabort a)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s1) (Handle e pes) (update_clock (\<lambda>_. 0) s', r'))
 7. \<And>ck env cn es vs s s' v1. do_con_check (c env) cn (length es) \<and> build_conv (c env) cn (rev vs) = Some v1 \<and> evaluate_list ck env s (rev es) (s', Rval vs) \<and> (\<forall>s'a r'. (s', Rval vs) = (s'a, r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_list True env (update_clock (\<lambda>_. c) s) (rev es) (update_clock (\<lambda>_. 0) s'a, r'))) \<Longrightarrow> \<forall>s'a r'. (s', Rval v1) = (s'a, r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) (Con cn es) (update_clock (\<lambda>_. 0) s'a, r'))
 8. \<And>ck env cn es s. \<not> do_con_check (c env) cn (length es) \<Longrightarrow> \<forall>s' r'. (s, Rerr (Rabort Rtype_error)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) (Con cn es) (update_clock (\<lambda>_. 0) s', r'))
 9. \<And>ck env cn es err s s'. do_con_check (c env) cn (length es) \<and> evaluate_list ck env s (rev es) (s', Rerr err) \<and> (\<forall>s'a r'. (s', Rerr err) = (s'a, r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_list True env (update_clock (\<lambda>_. c) s) (rev es) (update_clock (\<lambda>_. 0) s'a, r'))) \<Longrightarrow> \<forall>s'a r'. (s', Rerr err) = (s'a, r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) (Con cn es) (update_clock (\<lambda>_. 0) s'a, r'))
 10. \<And>ck env n v1 s. nsLookup (sem_env.v env) n = Some v1 \<Longrightarrow> \<forall>s' r'. (s, Rval v1) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) (Var n) (update_clock (\<lambda>_. 0) s', r'))
A total of 42 subgoals...
[PROOF STEP]
case app1
[PROOF STATE]
proof (state)
this:
(evaluate_list ck_ env_ s1_ (rev es_) (s2_, Rval vs_) \<and> (\<forall>s' r'. (s2_, Rval vs_) = (s', r') \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_list True env_ (update_clock (\<lambda>_. c) s1_) (rev es_) (update_clock (\<lambda>_. 0) s', r')))) \<and> do_opapp (rev vs_) = Some (env'_, e_) \<and> (ck_ \<longrightarrow> clock s2_ \<noteq> 0) \<and> evaluate ck_ env'_ (if ck_ then update_clock (\<lambda>_. clock s2_ - 1) s2_ else s2_) e_ bv_ \<and> (\<forall>s' r'. bv_ = (s', r') \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate True env'_ (update_clock (\<lambda>_. c) (if ck_ then update_clock (\<lambda>_. clock s2_ - 1) s2_ else s2_)) e_ (update_clock (\<lambda>_. 0) s', r')))

goal (42 subgoals):
 1. \<And>ck env l s. \<forall>s' r'. (s, Rval (Litv l)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) (Lit l) (update_clock (\<lambda>_. 0) s', r'))
 2. \<And>ck env e s1 s2 v1. \<lbrakk>evaluate ck s1 env e (s2, Rval v1); \<forall>s' r'. (s2, Rval v1) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) e (update_clock (\<lambda>_. 0) s', r'))\<rbrakk> \<Longrightarrow> \<forall>s' r'. (s2, Rerr (Rraise v1)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) (Raise e) (update_clock (\<lambda>_. 0) s', r'))
 3. \<And>ck env e s1 s2 err. \<lbrakk>evaluate ck s1 env e (s2, Rerr err); \<forall>s' r'. (s2, Rerr err) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) e (update_clock (\<lambda>_. 0) s', r'))\<rbrakk> \<Longrightarrow> \<forall>s' r'. (s2, Rerr err) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) (Raise e) (update_clock (\<lambda>_. 0) s', r'))
 4. \<And>ck s1 s2 env e v1 pes. \<lbrakk>evaluate ck s1 env e (s2, Rval v1); \<forall>s' r'. (s2, Rval v1) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) e (update_clock (\<lambda>_. 0) s', r'))\<rbrakk> \<Longrightarrow> \<forall>s' r'. (s2, Rval v1) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) (Handle e pes) (update_clock (\<lambda>_. 0) s', r'))
 5. \<And>ck s1 s2 env e pes v1 bv. (evaluate ck env s1 e (s2, Rerr (Rraise v1)) \<and> (\<forall>s' r'. (s2, Rerr (Rraise v1)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s1) e (update_clock (\<lambda>_. 0) s', r')))) \<and> evaluate_match ck env s2 v1 pes v1 bv \<and> (\<forall>s' r'. bv = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_match True env (update_clock (\<lambda>_. c) s2) v1 pes v1 (update_clock (\<lambda>_. 0) s', r'))) \<Longrightarrow> \<forall>s' r'. bv = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s1) (Handle e pes) (update_clock (\<lambda>_. 0) s', r'))
 6. \<And>ck s1 s2 env e pes a. \<lbrakk>evaluate ck env s1 e (s2, Rerr (Rabort a)); \<forall>s' r'. (s2, Rerr (Rabort a)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s1) e (update_clock (\<lambda>_. 0) s', r'))\<rbrakk> \<Longrightarrow> \<forall>s' r'. (s2, Rerr (Rabort a)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s1) (Handle e pes) (update_clock (\<lambda>_. 0) s', r'))
 7. \<And>ck env cn es vs s s' v1. do_con_check (c env) cn (length es) \<and> build_conv (c env) cn (rev vs) = Some v1 \<and> evaluate_list ck env s (rev es) (s', Rval vs) \<and> (\<forall>s'a r'. (s', Rval vs) = (s'a, r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_list True env (update_clock (\<lambda>_. c) s) (rev es) (update_clock (\<lambda>_. 0) s'a, r'))) \<Longrightarrow> \<forall>s'a r'. (s', Rval v1) = (s'a, r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) (Con cn es) (update_clock (\<lambda>_. 0) s'a, r'))
 8. \<And>ck env cn es s. \<not> do_con_check (c env) cn (length es) \<Longrightarrow> \<forall>s' r'. (s, Rerr (Rabort Rtype_error)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) (Con cn es) (update_clock (\<lambda>_. 0) s', r'))
 9. \<And>ck env cn es err s s'. do_con_check (c env) cn (length es) \<and> evaluate_list ck env s (rev es) (s', Rerr err) \<and> (\<forall>s'a r'. (s', Rerr err) = (s'a, r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_list True env (update_clock (\<lambda>_. c) s) (rev es) (update_clock (\<lambda>_. 0) s'a, r'))) \<Longrightarrow> \<forall>s'a r'. (s', Rerr err) = (s'a, r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) (Con cn es) (update_clock (\<lambda>_. 0) s'a, r'))
 10. \<And>ck env n v1 s. nsLookup (sem_env.v env) n = Some v1 \<Longrightarrow> \<forall>s' r'. (s, Rval v1) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) (Var n) (update_clock (\<lambda>_. 0) s', r'))
A total of 42 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(evaluate_list ck_ env_ s1_ (rev es_) (s2_, Rval vs_) \<and> (\<forall>s' r'. (s2_, Rval vs_) = (s', r') \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_list True env_ (update_clock (\<lambda>_. c) s1_) (rev es_) (update_clock (\<lambda>_. 0) s', r')))) \<and> do_opapp (rev vs_) = Some (env'_, e_) \<and> (ck_ \<longrightarrow> clock s2_ \<noteq> 0) \<and> evaluate ck_ env'_ (if ck_ then update_clock (\<lambda>_. clock s2_ - 1) s2_ else s2_) e_ bv_ \<and> (\<forall>s' r'. bv_ = (s', r') \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate True env'_ (update_clock (\<lambda>_. c) (if ck_ then update_clock (\<lambda>_. clock s2_ - 1) s2_ else s2_)) e_ (update_clock (\<lambda>_. 0) s', r')))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(evaluate_list ck_ env_ s1_ (rev es_) (s2_, Rval vs_) \<and> (\<forall>s' r'. (s2_, Rval vs_) = (s', r') \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate_list True env_ (update_clock (\<lambda>_. c) s1_) (rev es_) (update_clock (\<lambda>_. 0) s', r')))) \<and> do_opapp (rev vs_) = Some (env'_, e_) \<and> (ck_ \<longrightarrow> clock s2_ \<noteq> 0) \<and> evaluate ck_ env'_ (if ck_ then update_clock (\<lambda>_. clock s2_ - 1) s2_ else s2_) e_ bv_ \<and> (\<forall>s' r'. bv_ = (s', r') \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate True env'_ (update_clock (\<lambda>_. c) (if ck_ then update_clock (\<lambda>_. clock s2_ - 1) s2_ else s2_)) e_ (update_clock (\<lambda>_. 0) s', r')))

goal (1 subgoal):
 1. \<forall>s' r'. bv_ = (s', r') \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate True env_ (update_clock (\<lambda>_. c) s1_) (App Opapp es_) (update_clock (\<lambda>_. 0) s', r'))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s' r' c ca. \<lbrakk>evaluate_list False env_ s1_ (rev es_) (s2_, Rval vs_); do_opapp (rev vs_) = Some (env'_, e_); evaluate False env'_ s2_ e_ (s', r'); \<not> ck_; bv_ = (s', r'); evaluate_list True env_ (update_clock (\<lambda>_. c) s1_) (rev es_) (update_clock (\<lambda>_. 0) s2_, Rval vs_); evaluate True env'_ (update_clock (\<lambda>_. ca) s2_) e_ (update_clock (\<lambda>_. 0) s', r')\<rbrakk> \<Longrightarrow> \<exists>c. evaluate True env_ (update_clock (\<lambda>_. c) s1_) (App Opapp es_) (update_clock (\<lambda>_. 0) s', r')
[PROOF STEP]
subgoal for s' r' c c'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evaluate_list False env_ s1_ (rev es_) (s2_, Rval vs_); do_opapp (rev vs_) = Some (env'_, e_); evaluate False env'_ s2_ e_ (s', r'); \<not> ck_; bv_ = (s', r'); evaluate_list True env_ (update_clock (\<lambda>_. c) s1_) (rev es_) (update_clock (\<lambda>_. 0) s2_, Rval vs_); evaluate True env'_ (update_clock (\<lambda>_. c') s2_) e_ (update_clock (\<lambda>_. 0) s', r')\<rbrakk> \<Longrightarrow> \<exists>c. evaluate True env_ (update_clock (\<lambda>_. c) s1_) (App Opapp es_) (update_clock (\<lambda>_. 0) s', r')
[PROOF STEP]
apply (drule add_to_counter(2)[where extra = "c'+1"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>evaluate_list False env_ s1_ (rev es_) (s2_, Rval vs_); do_opapp (rev vs_) = Some (env'_, e_); evaluate False env'_ s2_ e_ (s', r'); \<not> ck_; bv_ = (s', r'); evaluate True env'_ (update_clock (\<lambda>_. c') s2_) e_ (update_clock (\<lambda>_. 0) s', r')\<rbrakk> \<Longrightarrow> Rval vs_ \<noteq> Rerr (Rabort Rtimeout_error)
 2. \<lbrakk>evaluate_list False env_ s1_ (rev es_) (s2_, Rval vs_); do_opapp (rev vs_) = Some (env'_, e_); evaluate False env'_ s2_ e_ (s', r'); \<not> ck_; bv_ = (s', r'); evaluate True env'_ (update_clock (\<lambda>_. c') s2_) e_ (update_clock (\<lambda>_. 0) s', r'); evaluate_list True env_ (update_clock (\<lambda>_. clock (update_clock (\<lambda>_. c) s1_) + (c' + 1)) (update_clock (\<lambda>_. c) s1_)) (rev es_) (update_clock (\<lambda>_. clock (update_clock (\<lambda>_. 0) s2_) + (c' + 1)) (update_clock (\<lambda>_. 0) s2_), Rval vs_)\<rbrakk> \<Longrightarrow> \<exists>c. evaluate True env_ (update_clock (\<lambda>_. c) s1_) (App Opapp es_) (update_clock (\<lambda>_. 0) s', r')
[PROOF STEP]
by (auto intro!: evaluate_match_evaluate_list_evaluate.intros)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>s' r'. bv_ = (s', r') \<and> ck_ = False \<longrightarrow> (\<exists>c. evaluate True env_ (update_clock (\<lambda>_. c) s1_) (App Opapp es_) (update_clock (\<lambda>_. 0) s', r'))

goal (41 subgoals):
 1. \<And>ck env l s. \<forall>s' r'. (s, Rval (Litv l)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) (Lit l) (update_clock (\<lambda>_. 0) s', r'))
 2. \<And>ck env e s1 s2 v1. \<lbrakk>evaluate ck s1 env e (s2, Rval v1); \<forall>s' r'. (s2, Rval v1) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) e (update_clock (\<lambda>_. 0) s', r'))\<rbrakk> \<Longrightarrow> \<forall>s' r'. (s2, Rerr (Rraise v1)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) (Raise e) (update_clock (\<lambda>_. 0) s', r'))
 3. \<And>ck env e s1 s2 err. \<lbrakk>evaluate ck s1 env e (s2, Rerr err); \<forall>s' r'. (s2, Rerr err) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) e (update_clock (\<lambda>_. 0) s', r'))\<rbrakk> \<Longrightarrow> \<forall>s' r'. (s2, Rerr err) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) (Raise e) (update_clock (\<lambda>_. 0) s', r'))
 4. \<And>ck s1 s2 env e v1 pes. \<lbrakk>evaluate ck s1 env e (s2, Rval v1); \<forall>s' r'. (s2, Rval v1) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) e (update_clock (\<lambda>_. 0) s', r'))\<rbrakk> \<Longrightarrow> \<forall>s' r'. (s2, Rval v1) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True s1 (update_clock (\<lambda>_. c) env) (Handle e pes) (update_clock (\<lambda>_. 0) s', r'))
 5. \<And>ck s1 s2 env e pes v1 bv. (evaluate ck env s1 e (s2, Rerr (Rraise v1)) \<and> (\<forall>s' r'. (s2, Rerr (Rraise v1)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s1) e (update_clock (\<lambda>_. 0) s', r')))) \<and> evaluate_match ck env s2 v1 pes v1 bv \<and> (\<forall>s' r'. bv = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_match True env (update_clock (\<lambda>_. c) s2) v1 pes v1 (update_clock (\<lambda>_. 0) s', r'))) \<Longrightarrow> \<forall>s' r'. bv = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s1) (Handle e pes) (update_clock (\<lambda>_. 0) s', r'))
 6. \<And>ck s1 s2 env e pes a. \<lbrakk>evaluate ck env s1 e (s2, Rerr (Rabort a)); \<forall>s' r'. (s2, Rerr (Rabort a)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s1) e (update_clock (\<lambda>_. 0) s', r'))\<rbrakk> \<Longrightarrow> \<forall>s' r'. (s2, Rerr (Rabort a)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s1) (Handle e pes) (update_clock (\<lambda>_. 0) s', r'))
 7. \<And>ck env cn es vs s s' v1. do_con_check (c env) cn (length es) \<and> build_conv (c env) cn (rev vs) = Some v1 \<and> evaluate_list ck env s (rev es) (s', Rval vs) \<and> (\<forall>s'a r'. (s', Rval vs) = (s'a, r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_list True env (update_clock (\<lambda>_. c) s) (rev es) (update_clock (\<lambda>_. 0) s'a, r'))) \<Longrightarrow> \<forall>s'a r'. (s', Rval v1) = (s'a, r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) (Con cn es) (update_clock (\<lambda>_. 0) s'a, r'))
 8. \<And>ck env cn es s. \<not> do_con_check (c env) cn (length es) \<Longrightarrow> \<forall>s' r'. (s, Rerr (Rabort Rtype_error)) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) (Con cn es) (update_clock (\<lambda>_. 0) s', r'))
 9. \<And>ck env cn es err s s'. do_con_check (c env) cn (length es) \<and> evaluate_list ck env s (rev es) (s', Rerr err) \<and> (\<forall>s'a r'. (s', Rerr err) = (s'a, r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate_list True env (update_clock (\<lambda>_. c) s) (rev es) (update_clock (\<lambda>_. 0) s'a, r'))) \<Longrightarrow> \<forall>s'a r'. (s', Rerr err) = (s'a, r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) (Con cn es) (update_clock (\<lambda>_. 0) s'a, r'))
 10. \<And>ck env n v1 s. nsLookup (sem_env.v env) n = Some v1 \<Longrightarrow> \<forall>s' r'. (s, Rval v1) = (s', r') \<and> ck = False \<longrightarrow> (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) (Var n) (update_clock (\<lambda>_. 0) s', r'))
A total of 41 subgoals...
[PROOF STEP]
qed (force intro: evaluate_match_evaluate_list_evaluate.intros dest:add_to_counter(3))+


[STATEMENT]
lemma clock_monotone:
  "evaluate_match ck env s v pes err_v r1 \<Longrightarrow> \<forall>s' r'. r1 = (s',r') \<and> (ck=True) \<longrightarrow> (clock   s') \<le> (clock   s)"
  "evaluate_list ck env s es r2 \<Longrightarrow> \<forall>s' r'. r2 = (s',r') \<and> (ck = True) \<longrightarrow> (clock   s') \<le> (clock   s)"
  "evaluate ck env s e r3 \<Longrightarrow> \<forall>s' r'. r3 = (s',r') \<and> (ck = True) \<longrightarrow> (clock   s') \<le> (clock   s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (evaluate_match ck env s v pes err_v r1 \<Longrightarrow> \<forall>s' r'. r1 = (s', r') \<and> ck = True \<longrightarrow> clock s' \<le> clock s) &&& (evaluate_list ck env s es r2 \<Longrightarrow> \<forall>s' r'. r2 = (s', r') \<and> ck = True \<longrightarrow> clock s' \<le> clock s) &&& (evaluate ck env s e r3 \<Longrightarrow> \<forall>s' r'. r3 = (s', r') \<and> ck = True \<longrightarrow> clock s' \<le> clock s)
[PROOF STEP]
by (induction rule:evaluate_match_evaluate_list_evaluate.inducts) auto


[STATEMENT]
lemma big_clocked_unclocked_equiv:
  "evaluate False env s e (s',r1) =
   (\<exists>c. evaluate True env (s (| clock := c |)) e ((s' (| clock := 0 |)),r1) \<and>
        r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> (clock   s) = (clock   s'))" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate False env s e (s', r1) = (\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1) \<and> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. evaluate False env s e (s', r1) \<Longrightarrow> \<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1) \<and> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
 2. \<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1) \<and> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s' \<Longrightarrow> evaluate False env s e (s', r1)
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
evaluate False env s e (s', r1)

goal (2 subgoals):
 1. evaluate False env s e (s', r1) \<Longrightarrow> \<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1) \<and> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
 2. \<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1) \<and> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s' \<Longrightarrow> evaluate False env s e (s', r1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate False env s e (s', r1)
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
evaluate False env s e (s', r1)

goal (1 subgoal):
 1. \<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1) \<and> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
using big_unclocked_unchanged(3)
[PROOF STATE]
proof (prove)
using this:
evaluate False env s e (s', r1)
evaluate False ?env ?s ?e (?s', ?r3.0) \<Longrightarrow> clock ?s = clock ?s'

goal (1 subgoal):
 1. \<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1) \<and> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
by (fastforce simp add: big_unclocked_unchanged big_unclocked_notimeout add_clock)
[PROOF STATE]
proof (state)
this:
\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1) \<and> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'

goal (1 subgoal):
 1. \<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1) \<and> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s' \<Longrightarrow> evaluate False env s e (s', r1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1) \<and> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s' \<Longrightarrow> evaluate False env s e (s', r1)
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1) \<and> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'

goal (1 subgoal):
 1. \<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1) \<and> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s' \<Longrightarrow> evaluate False env s e (s', r1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1) \<and> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
\<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1) \<and> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s'

goal (1 subgoal):
 1. evaluate False env s e (s', r1)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1) \<and> r1 \<noteq> Rerr (Rabort Rtimeout_error) \<and> clock s = clock s' \<Longrightarrow> evaluate False env s e (s', r1)
[PROOF STEP]
apply (elim conjE exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>evaluate True env (update_clock (\<lambda>_. c) s) e (update_clock (\<lambda>_. 0) s', r1); r1 \<noteq> Rerr (Rabort Rtimeout_error); clock s = clock s'\<rbrakk> \<Longrightarrow> evaluate False env s e (s', r1)
[PROOF STEP]
apply (drule big_unclocked_ignore(3))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>r1 \<noteq> Rerr (Rabort Rtimeout_error); clock s = clock s'\<rbrakk> \<Longrightarrow> r1 \<noteq> Rerr (Rabort Rtimeout_error)
 2. \<And>c. \<lbrakk>r1 \<noteq> Rerr (Rabort Rtimeout_error); clock s = clock s'; evaluate False env (update_clock (\<lambda>_. ?cnt4 c) (update_clock (\<lambda>_. c) s)) e (update_clock (\<lambda>_. ?cnt4 c) (update_clock (\<lambda>_. 0) s'), r1)\<rbrakk> \<Longrightarrow> evaluate False env s e (s', r1)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>r1 \<noteq> Rerr (Rabort Rtimeout_error); clock s = clock s'; evaluate False env (update_clock (\<lambda>a. ?cnt4 c) s) e (update_clock (\<lambda>a. ?cnt4 c) s', r1)\<rbrakk> \<Longrightarrow> evaluate False env s e (s', r1)
[PROOF STEP]
by (metis big_unclocked state.record_simps(7))
[PROOF STATE]
proof (state)
this:
evaluate False env s e (s', r1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma big_clocked_timeout_0:
  "evaluate_match ck env s v pes err_v r1  \<Longrightarrow> \<forall>s'. r1 = (s',Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> (clock s') = 0"
  "evaluate_list ck env s es r2  \<Longrightarrow> \<forall>s'. r2 = (s',Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> (clock s') = 0"
  "evaluate ck env s e r3  \<Longrightarrow> \<forall>s'. r3 = (s',Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> (clock s') = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (evaluate_match ck env s v pes err_v r1 \<Longrightarrow> \<forall>s'. r1 = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0) &&& (evaluate_list ck env s es r2 \<Longrightarrow> \<forall>s'. r2 = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0) &&& (evaluate ck env s e r3 \<Longrightarrow> \<forall>s'. r3 = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0)
[PROOF STEP]
proof(induction rule:evaluate_match_evaluate_list_evaluate.inducts)
[PROOF STATE]
proof (state)
goal (42 subgoals):
 1. \<And>ck env l s. \<forall>s'. (s, Rval (Litv l)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 2. \<And>ck env e s1 s2 v1. \<lbrakk>evaluate ck s1 env e (s2, Rval v1); \<forall>s'. (s2, Rval v1) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0\<rbrakk> \<Longrightarrow> \<forall>s'. (s2, Rerr (Rraise v1)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 3. \<And>ck env e s1 s2 err. \<lbrakk>evaluate ck s1 env e (s2, Rerr err); \<forall>s'. (s2, Rerr err) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0\<rbrakk> \<Longrightarrow> \<forall>s'. (s2, Rerr err) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 4. \<And>ck s1 s2 env e v1 pes. \<lbrakk>evaluate ck s1 env e (s2, Rval v1); \<forall>s'. (s2, Rval v1) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0\<rbrakk> \<Longrightarrow> \<forall>s'. (s2, Rval v1) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 5. \<And>ck s1 s2 env e pes v1 bv. (evaluate ck env s1 e (s2, Rerr (Rraise v1)) \<and> (\<forall>s'. (s2, Rerr (Rraise v1)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0)) \<and> evaluate_match ck env s2 v1 pes v1 bv \<and> (\<forall>s'. bv = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0) \<Longrightarrow> \<forall>s'. bv = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 6. \<And>ck s1 s2 env e pes a. \<lbrakk>evaluate ck env s1 e (s2, Rerr (Rabort a)); \<forall>s'. (s2, Rerr (Rabort a)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0\<rbrakk> \<Longrightarrow> \<forall>s'. (s2, Rerr (Rabort a)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 7. \<And>ck env cn es vs s s' v1. do_con_check (c env) cn (length es) \<and> build_conv (c env) cn (rev vs) = Some v1 \<and> evaluate_list ck env s (rev es) (s', Rval vs) \<and> (\<forall>s'a. (s', Rval vs) = (s'a, Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s'a = 0) \<Longrightarrow> \<forall>s'a. (s', Rval v1) = (s'a, Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s'a = 0
 8. \<And>ck env cn es s. \<not> do_con_check (c env) cn (length es) \<Longrightarrow> \<forall>s'. (s, Rerr (Rabort Rtype_error)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 9. \<And>ck env cn es err s s'. do_con_check (c env) cn (length es) \<and> evaluate_list ck env s (rev es) (s', Rerr err) \<and> (\<forall>s'a. (s', Rerr err) = (s'a, Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s'a = 0) \<Longrightarrow> \<forall>s'a. (s', Rerr err) = (s'a, Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s'a = 0
 10. \<And>ck env n v1 s. nsLookup (sem_env.v env) n = Some v1 \<Longrightarrow> \<forall>s'. (s, Rval v1) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
A total of 42 subgoals...
[PROOF STEP]
case app4
[PROOF STATE]
proof (state)
this:
(evaluate_list ck_ env_ s1_ (rev es_) (s2_, Rval vs_) \<and> (\<forall>s'. (s2_, Rval vs_) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck_ = True \<longrightarrow> clock s' = 0)) \<and> do_app (refs s2_, ffi s2_) op0_ (rev vs_) = Some ((refs'_, ffi'_), res_) \<and> op0_ \<noteq> Opapp

goal (42 subgoals):
 1. \<And>ck env l s. \<forall>s'. (s, Rval (Litv l)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 2. \<And>ck env e s1 s2 v1. \<lbrakk>evaluate ck s1 env e (s2, Rval v1); \<forall>s'. (s2, Rval v1) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0\<rbrakk> \<Longrightarrow> \<forall>s'. (s2, Rerr (Rraise v1)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 3. \<And>ck env e s1 s2 err. \<lbrakk>evaluate ck s1 env e (s2, Rerr err); \<forall>s'. (s2, Rerr err) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0\<rbrakk> \<Longrightarrow> \<forall>s'. (s2, Rerr err) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 4. \<And>ck s1 s2 env e v1 pes. \<lbrakk>evaluate ck s1 env e (s2, Rval v1); \<forall>s'. (s2, Rval v1) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0\<rbrakk> \<Longrightarrow> \<forall>s'. (s2, Rval v1) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 5. \<And>ck s1 s2 env e pes v1 bv. (evaluate ck env s1 e (s2, Rerr (Rraise v1)) \<and> (\<forall>s'. (s2, Rerr (Rraise v1)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0)) \<and> evaluate_match ck env s2 v1 pes v1 bv \<and> (\<forall>s'. bv = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0) \<Longrightarrow> \<forall>s'. bv = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 6. \<And>ck s1 s2 env e pes a. \<lbrakk>evaluate ck env s1 e (s2, Rerr (Rabort a)); \<forall>s'. (s2, Rerr (Rabort a)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0\<rbrakk> \<Longrightarrow> \<forall>s'. (s2, Rerr (Rabort a)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 7. \<And>ck env cn es vs s s' v1. do_con_check (c env) cn (length es) \<and> build_conv (c env) cn (rev vs) = Some v1 \<and> evaluate_list ck env s (rev es) (s', Rval vs) \<and> (\<forall>s'a. (s', Rval vs) = (s'a, Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s'a = 0) \<Longrightarrow> \<forall>s'a. (s', Rval v1) = (s'a, Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s'a = 0
 8. \<And>ck env cn es s. \<not> do_con_check (c env) cn (length es) \<Longrightarrow> \<forall>s'. (s, Rerr (Rabort Rtype_error)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 9. \<And>ck env cn es err s s'. do_con_check (c env) cn (length es) \<and> evaluate_list ck env s (rev es) (s', Rerr err) \<and> (\<forall>s'a. (s', Rerr err) = (s'a, Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s'a = 0) \<Longrightarrow> \<forall>s'a. (s', Rerr err) = (s'a, Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s'a = 0
 10. \<And>ck env n v1 s. nsLookup (sem_env.v env) n = Some v1 \<Longrightarrow> \<forall>s'. (s, Rval v1) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
A total of 42 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(evaluate_list ck_ env_ s1_ (rev es_) (s2_, Rval vs_) \<and> (\<forall>s'. (s2_, Rval vs_) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck_ = True \<longrightarrow> clock s' = 0)) \<and> do_app (refs s2_, ffi s2_) op0_ (rev vs_) = Some ((refs'_, ffi'_), res_) \<and> op0_ \<noteq> Opapp
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(evaluate_list ck_ env_ s1_ (rev es_) (s2_, Rval vs_) \<and> (\<forall>s'. (s2_, Rval vs_) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck_ = True \<longrightarrow> clock s' = 0)) \<and> do_app (refs s2_, ffi s2_) op0_ (rev vs_) = Some ((refs'_, ffi'_), res_) \<and> op0_ \<noteq> Opapp

goal (1 subgoal):
 1. \<forall>s'. (update_ffi (\<lambda>_. ffi'_) (update_refs (\<lambda>_. refs'_) s2_), res_) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck_ = True \<longrightarrow> clock s' = 0
[PROOF STEP]
by (auto dest!:do_app_no_runtime_error)
[PROOF STATE]
proof (state)
this:
\<forall>s'. (update_ffi (\<lambda>_. ffi'_) (update_refs (\<lambda>_. refs'_) s2_), res_) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck_ = True \<longrightarrow> clock s' = 0

goal (41 subgoals):
 1. \<And>ck env l s. \<forall>s'. (s, Rval (Litv l)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 2. \<And>ck env e s1 s2 v1. \<lbrakk>evaluate ck s1 env e (s2, Rval v1); \<forall>s'. (s2, Rval v1) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0\<rbrakk> \<Longrightarrow> \<forall>s'. (s2, Rerr (Rraise v1)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 3. \<And>ck env e s1 s2 err. \<lbrakk>evaluate ck s1 env e (s2, Rerr err); \<forall>s'. (s2, Rerr err) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0\<rbrakk> \<Longrightarrow> \<forall>s'. (s2, Rerr err) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 4. \<And>ck s1 s2 env e v1 pes. \<lbrakk>evaluate ck s1 env e (s2, Rval v1); \<forall>s'. (s2, Rval v1) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0\<rbrakk> \<Longrightarrow> \<forall>s'. (s2, Rval v1) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 5. \<And>ck s1 s2 env e pes v1 bv. (evaluate ck env s1 e (s2, Rerr (Rraise v1)) \<and> (\<forall>s'. (s2, Rerr (Rraise v1)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0)) \<and> evaluate_match ck env s2 v1 pes v1 bv \<and> (\<forall>s'. bv = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0) \<Longrightarrow> \<forall>s'. bv = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 6. \<And>ck s1 s2 env e pes a. \<lbrakk>evaluate ck env s1 e (s2, Rerr (Rabort a)); \<forall>s'. (s2, Rerr (Rabort a)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0\<rbrakk> \<Longrightarrow> \<forall>s'. (s2, Rerr (Rabort a)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 7. \<And>ck env cn es vs s s' v1. do_con_check (c env) cn (length es) \<and> build_conv (c env) cn (rev vs) = Some v1 \<and> evaluate_list ck env s (rev es) (s', Rval vs) \<and> (\<forall>s'a. (s', Rval vs) = (s'a, Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s'a = 0) \<Longrightarrow> \<forall>s'a. (s', Rval v1) = (s'a, Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s'a = 0
 8. \<And>ck env cn es s. \<not> do_con_check (c env) cn (length es) \<Longrightarrow> \<forall>s'. (s, Rerr (Rabort Rtype_error)) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
 9. \<And>ck env cn es err s s'. do_con_check (c env) cn (length es) \<and> evaluate_list ck env s (rev es) (s', Rerr err) \<and> (\<forall>s'a. (s', Rerr err) = (s'a, Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s'a = 0) \<Longrightarrow> \<forall>s'a. (s', Rerr err) = (s'a, Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s'a = 0
 10. \<And>ck env n v1 s. nsLookup (sem_env.v env) n = Some v1 \<Longrightarrow> \<forall>s'. (s, Rval v1) = (s', Rerr (Rabort Rtimeout_error)) \<and> ck = True \<longrightarrow> clock s' = 0
A total of 41 subgoals...
[PROOF STEP]
qed(auto)


[STATEMENT]
lemma big_clocked_unclocked_equiv_timeout:
  "(\<forall>r. \<not>evaluate False env s e r) =
   (\<forall>c. \<exists>s'. evaluate True env (s \<lparr> clock := c \<rparr>) e (s',Rerr (Rabort Rtimeout_error)) \<and> (clock s') = 0)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>r. \<not> evaluate False env s e r) = (\<forall>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0)
[PROOF STEP]
proof rule
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>r. \<not> evaluate False env s e r \<Longrightarrow> \<forall>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0
 2. \<forall>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0 \<Longrightarrow> \<forall>r. \<not> evaluate False env s e r
[PROOF STEP]
assume l:?lhs
[PROOF STATE]
proof (state)
this:
\<forall>r. \<not> evaluate False env s e r

goal (2 subgoals):
 1. \<forall>r. \<not> evaluate False env s e r \<Longrightarrow> \<forall>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0
 2. \<forall>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0 \<Longrightarrow> \<forall>r. \<not> evaluate False env s e r
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0
[PROOF STEP]
obtain s' r where e:"evaluate True env (update_clock (\<lambda>_. c) s) e (s',r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s' r. evaluate True env (update_clock (\<lambda>_. c) s) e (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using evaluate_total
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate True ?env ?s ?e (s', r)

goal (1 subgoal):
 1. (\<And>s' r. evaluate True env (update_clock (\<lambda>_. c) s) e (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
evaluate True env (update_clock (\<lambda>_. c) s) e (s', r)

goal (1 subgoal):
 1. \<And>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0
[PROOF STEP]
have r:"r = Rerr (Rabort Rtimeout_error)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
using l big_unclocked_ignore(3)[OF e, simplified]
[PROOF STATE]
proof (prove)
using this:
\<forall>r. \<not> evaluate False env s e r
r \<noteq> Rerr (Rabort Rtimeout_error) \<Longrightarrow> evaluate False env (update_clock (\<lambda>a. ?cnt) s) e (update_clock (\<lambda>_. ?cnt) s', r)

goal (1 subgoal):
 1. r = Rerr (Rabort Rtimeout_error)
[PROOF STEP]
by (metis state.record_simps(7))
[PROOF STATE]
proof (state)
this:
r = Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. \<And>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r = Rerr (Rabort Rtimeout_error)

goal (1 subgoal):
 1. \<And>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0
[PROOF STEP]
have "(clock s') = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clock s' = 0
[PROOF STEP]
using r e big_clocked_timeout_0(3)
[PROOF STATE]
proof (prove)
using this:
r = Rerr (Rabort Rtimeout_error)
evaluate True env (update_clock (\<lambda>_. c) s) e (s', r)
evaluate ?ck ?env ?s ?e ?r3.0 \<Longrightarrow> \<forall>s'. ?r3.0 = (s', Rerr (Rabort Rtimeout_error)) \<and> ?ck = True \<longrightarrow> clock s' = 0

goal (1 subgoal):
 1. clock s' = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
clock s' = 0

goal (1 subgoal):
 1. \<And>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r = Rerr (Rabort Rtimeout_error)
clock s' = 0
[PROOF STEP]
show "\<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0"
[PROOF STATE]
proof (prove)
using this:
r = Rerr (Rabort Rtimeout_error)
clock s' = 0

goal (1 subgoal):
 1. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
r = Rerr (Rabort Rtimeout_error)
clock s' = 0
evaluate True env (update_clock (\<lambda>_. c) s) e (s', r)

goal (1 subgoal):
 1. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0

goal (1 subgoal):
 1. \<forall>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0 \<Longrightarrow> \<forall>r. \<not> evaluate False env s e r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0 \<Longrightarrow> \<forall>r. \<not> evaluate False env s e r
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
\<forall>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0

goal (1 subgoal):
 1. \<forall>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0 \<Longrightarrow> \<forall>r. \<not> evaluate False env s e r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
\<forall>c. \<exists>s'. evaluate True env (update_clock (\<lambda>_. c) s) e (s', Rerr (Rabort Rtimeout_error)) \<and> clock s' = 0

goal (1 subgoal):
 1. \<forall>r. \<not> evaluate False env s e r
[PROOF STEP]
by (metis big_clocked_unclocked_equiv eq_snd_iff evaluate_determ(3))
[PROOF STATE]
proof (state)
this:
\<forall>r. \<not> evaluate False env s e r

goal:
No subgoals!
[PROOF STEP]
qed