[STATEMENT]
lemma padic_int_is_cring:
  assumes "prime p"
  shows "cring (padic_int p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring (padic_int p)
[PROOF STEP]
proof (rule cringI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. abelian_group (padic_int p)
 2. Group.comm_monoid (padic_int p)
 3. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
show "abelian_group (padic_int p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abelian_group (padic_int p)
[PROOF STEP]
by (simp add: assms padic_is_abelian_group)
[PROOF STATE]
proof (state)
this:
abelian_group (padic_int p)

goal (2 subgoals):
 1. Group.comm_monoid (padic_int p)
 2. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
show "Group.comm_monoid (padic_int p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group.comm_monoid (padic_int p)
[PROOF STEP]
by (simp add: assms padic_is_comm_monoid)
[PROOF STATE]
proof (state)
this:
Group.comm_monoid (padic_int p)

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
show "\<And>x y z.
       x \<in> carrier (padic_int p) \<Longrightarrow>
       y \<in> carrier (padic_int p) \<Longrightarrow>
       z \<in> carrier (padic_int p) \<Longrightarrow>
       (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z =
         x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
fix x y z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
assume Ax: " x \<in> carrier (padic_int p)"
[PROOF STATE]
proof (state)
this:
x \<in> carrier (padic_int p)

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
assume Ay: " y \<in> carrier (padic_int p)"
[PROOF STATE]
proof (state)
this:
y \<in> carrier (padic_int p)

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
assume Az: " z \<in> carrier (padic_int p)"
[PROOF STATE]
proof (state)
this:
z \<in> carrier (padic_int p)

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<in> carrier (padic_int p); y \<in> carrier (padic_int p); z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
show "(x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z
          = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) xa = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) xa
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) xa = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) xa
[PROOF STEP]
have Ex: " (x n) \<in> carrier (residue_ring (p^n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x n \<in> carrier (residue_ring (p ^ n))
[PROOF STEP]
using Ax padic_set_def padic_int_simps
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier (padic_int p)
padic_set ?p = {f. (\<forall>m. f m \<in> carrier (residue_ring (?p ^ m))) \<and> (\<forall>n m. m < n \<longrightarrow> residue (?p ^ m) (f n) = f m)}
\<one>\<^bsub>padic_int ?p\<^esub> = padic_one ?p
\<zero>\<^bsub>padic_int ?p\<^esub> = padic_zero ?p
(\<oplus>\<^bsub>padic_int ?p\<^esub>) = padic_add ?p
(\<otimes>\<^bsub>padic_int ?p\<^esub>) = padic_mult ?p
carrier (padic_int ?p) = padic_set ?p

goal (1 subgoal):
 1. x n \<in> carrier (residue_ring (p ^ n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x n \<in> carrier (residue_ring (p ^ n))

goal (1 subgoal):
 1. \<And>xa. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) xa = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) xa
[PROOF STEP]
have Ey: " (y n) \<in> carrier (residue_ring (p^n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y n \<in> carrier (residue_ring (p ^ n))
[PROOF STEP]
using Ay padic_set_def padic_int_simps
[PROOF STATE]
proof (prove)
using this:
y \<in> carrier (padic_int p)
padic_set ?p = {f. (\<forall>m. f m \<in> carrier (residue_ring (?p ^ m))) \<and> (\<forall>n m. m < n \<longrightarrow> residue (?p ^ m) (f n) = f m)}
\<one>\<^bsub>padic_int ?p\<^esub> = padic_one ?p
\<zero>\<^bsub>padic_int ?p\<^esub> = padic_zero ?p
(\<oplus>\<^bsub>padic_int ?p\<^esub>) = padic_add ?p
(\<otimes>\<^bsub>padic_int ?p\<^esub>) = padic_mult ?p
carrier (padic_int ?p) = padic_set ?p

goal (1 subgoal):
 1. y n \<in> carrier (residue_ring (p ^ n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y n \<in> carrier (residue_ring (p ^ n))

goal (1 subgoal):
 1. \<And>xa. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) xa = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) xa
[PROOF STEP]
have Ez: " (z n) \<in> carrier (residue_ring (p^n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z n \<in> carrier (residue_ring (p ^ n))
[PROOF STEP]
using Az padic_set_def padic_int_simps
[PROOF STATE]
proof (prove)
using this:
z \<in> carrier (padic_int p)
padic_set ?p = {f. (\<forall>m. f m \<in> carrier (residue_ring (?p ^ m))) \<and> (\<forall>n m. m < n \<longrightarrow> residue (?p ^ m) (f n) = f m)}
\<one>\<^bsub>padic_int ?p\<^esub> = padic_one ?p
\<zero>\<^bsub>padic_int ?p\<^esub> = padic_zero ?p
(\<oplus>\<^bsub>padic_int ?p\<^esub>) = padic_add ?p
(\<otimes>\<^bsub>padic_int ?p\<^esub>) = padic_mult ?p
carrier (padic_int ?p) = padic_set ?p

goal (1 subgoal):
 1. z n \<in> carrier (residue_ring (p ^ n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z n \<in> carrier (residue_ring (p ^ n))

goal (1 subgoal):
 1. \<And>xa. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) xa = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) xa
[PROOF STEP]
show "( (x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n
            = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
proof(cases "n=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
 2. n \<noteq> 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
 2. n \<noteq> 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
by (metis Ax Ay Az assms padic_add_closed padic_int_simps(4) padic_int_simps(5) padic_mult_in_padic_set padic_set_zero_res)
[PROOF STATE]
proof (state)
this:
((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0
[PROOF STEP]
have "residues (p^n)"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. residues (p ^ n)
[PROOF STEP]
by (simp add: assms residues_n)
[PROOF STATE]
proof (state)
this:
residues (p ^ n)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
residues (p ^ n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
residues (p ^ n)

goal (1 subgoal):
 1. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
using Ex Ey Ez cring.cring_simprules(13) padic_add_res padic_int_simps
            padic_mult_res residues.cring
[PROOF STATE]
proof (prove)
using this:
residues (p ^ n)
x n \<in> carrier (residue_ring (p ^ n))
y n \<in> carrier (residue_ring (p ^ n))
z n \<in> carrier (residue_ring (p ^ n))
\<lbrakk>cring ?R; ?x \<in> carrier ?R; ?y \<in> carrier ?R; ?z \<in> carrier ?R\<rbrakk> \<Longrightarrow> (?x \<oplus>\<^bsub>?R\<^esub> ?y) \<otimes>\<^bsub>?R\<^esub> ?z = ?x \<otimes>\<^bsub>?R\<^esub> ?z \<oplus>\<^bsub>?R\<^esub> ?y \<otimes>\<^bsub>?R\<^esub> ?z
padic_add ?p ?f ?g ?n = ?f ?n \<oplus>\<^bsub>residue_ring (?p ^ ?n)\<^esub> ?g ?n
\<one>\<^bsub>padic_int ?p\<^esub> = padic_one ?p
\<zero>\<^bsub>padic_int ?p\<^esub> = padic_zero ?p
(\<oplus>\<^bsub>padic_int ?p\<^esub>) = padic_add ?p
(\<otimes>\<^bsub>padic_int ?p\<^esub>) = padic_mult ?p
carrier (padic_int ?p) = padic_set ?p
padic_mult ?p ?f ?g ?n = ?f ?n \<otimes>\<^bsub>residue_ring (?p ^ ?n)\<^esub> ?g ?n
residues ?m \<Longrightarrow> cring (residue_ring ?m)

goal (1 subgoal):
 1. ((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z) n = (x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z) n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x \<oplus>\<^bsub>padic_int p\<^esub> y) \<otimes>\<^bsub>padic_int p\<^esub> z = x \<otimes>\<^bsub>padic_int p\<^esub> z \<oplus>\<^bsub>padic_int p\<^esub> y \<otimes>\<^bsub>padic_int p\<^esub> z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> carrier (padic_int p); ?y \<in> carrier (padic_int p); ?z \<in> carrier (padic_int p)\<rbrakk> \<Longrightarrow> (?x \<oplus>\<^bsub>padic_int p\<^esub> ?y) \<otimes>\<^bsub>padic_int p\<^esub> ?z = ?x \<otimes>\<^bsub>padic_int p\<^esub> ?z \<oplus>\<^bsub>padic_int p\<^esub> ?y \<otimes>\<^bsub>padic_int p\<^esub> ?z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma store_cond_cap:
  assumes "store h c val = Success h'"
    and "val = Cap_v v"
  shows "\<exists> m. Mapping.lookup (heap_map h') (block_id c) = Some (Map m)
          \<and> offset c \<ge> fst (bounds m)
          \<and> offset c + |memval_type val|\<^sub>\<tau> \<le> snd (bounds m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. Mapping.lookup (heap_map h') (block_id c) = Some (Map m) \<and> int (fst (bounds m)) \<le> offset c \<and> offset c + int |memval_type val|\<^sub>\<tau> \<le> int (snd (bounds m))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m. Mapping.lookup (heap_map h') (block_id c) = Some (Map m) \<and> int (fst (bounds m)) \<le> offset c \<and> offset c + int |memval_type val|\<^sub>\<tau> \<le> int (snd (bounds m))
[PROOF STEP]
have cap_perms: "\<not>(\<not> perm_cap_store c \<and> tag v) \<and> \<not>(\<not> perm_cap_store_local c \<and> tag v \<and> \<not> perm_global v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<not> perm_cap_store c \<and> tag v) \<and> \<not> (\<not> perm_cap_store_local c \<and> tag v \<and> \<not> perm_global v)
[PROOF STEP]
using store_cond_hard_cap(1)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(2)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(3)[where ?h=h and ?c=c and ?v=val and ?ret=h' and ?cv=v, OF assms(1)]
      store_cond_hard_cap(4)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(5)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(6)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      assms
[PROOF STATE]
proof (prove)
using this:
tag c = True
perm_store c = True
\<lbrakk>val = Cap_v v; tag v\<rbrakk> \<Longrightarrow> perm_cap_store c \<and> (perm_cap_store_local c \<or> perm_global v)
offset c + int |memval_type val|\<^sub>\<tau> \<le> int (base c + len c)
int (base c) \<le> offset c
offset c mod int |memval_type val|\<^sub>\<tau> = 0
store h c val = Success h'
val = Cap_v v

goal (1 subgoal):
 1. \<not> (\<not> perm_cap_store c \<and> tag v) \<and> \<not> (\<not> perm_cap_store_local c \<and> tag v \<and> \<not> perm_global v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> (\<not> perm_cap_store c \<and> tag v) \<and> \<not> (\<not> perm_cap_store_local c \<and> tag v \<and> \<not> perm_global v)

goal (1 subgoal):
 1. \<exists>m. Mapping.lookup (heap_map h') (block_id c) = Some (Map m) \<and> int (fst (bounds m)) \<le> offset c \<and> offset c + int |memval_type val|\<^sub>\<tau> \<le> int (snd (bounds m))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. Mapping.lookup (heap_map h') (block_id c) = Some (Map m) \<and> int (fst (bounds m)) \<le> offset c \<and> offset c + int |memval_type val|\<^sub>\<tau> \<le> int (snd (bounds m))
[PROOF STEP]
using store_cond_hard_cap(1)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(2)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(3)[where ?h=h and ?c=c and ?v=val and ?ret=h' and ?cv=v, OF assms(1)]
      store_cond_hard_cap(4)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(5)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(6)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      assms
[PROOF STATE]
proof (prove)
using this:
tag c = True
perm_store c = True
\<lbrakk>val = Cap_v v; tag v\<rbrakk> \<Longrightarrow> perm_cap_store c \<and> (perm_cap_store_local c \<or> perm_global v)
offset c + int |memval_type val|\<^sub>\<tau> \<le> int (base c + len c)
int (base c) \<le> offset c
offset c mod int |memval_type val|\<^sub>\<tau> = 0
store h c val = Success h'
val = Cap_v v

goal (1 subgoal):
 1. \<exists>m. Mapping.lookup (heap_map h') (block_id c) = Some (Map m) \<and> int (fst (bounds m)) \<le> offset c \<and> offset c + int |memval_type val|\<^sub>\<tau> \<le> int (snd (bounds m))
[PROOF STEP]
by (clarsimp split: ccval.split option.split_asm t.split_asm simp add: store_def cap_perms)
      (smt (verit) Mapping.lookup_update assms(1) result.distinct(1) result.sel(1) store_bound_violated_2 store_cond_hard_cap(3) store_def store_success store_tval_disjoint_bounds)
[PROOF STATE]
proof (state)
this:
\<exists>m. Mapping.lookup (heap_map h') (block_id c) = Some (Map m) \<and> int (fst (bounds m)) \<le> offset c \<and> offset c + int |memval_type val|\<^sub>\<tau> \<le> int (snd (bounds m))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv2_param[param]: "(inv2,inv2)\<in>\<langle>Rk,Rv\<rangle>rbt_rel\<rightarrow>Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inv2, inv2) \<in> \<langle>Rk, Rv\<rangle>rbt_rel \<rightarrow> bool_rel
[PROOF STEP]
unfolding inv2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rec_rbt True (\<lambda>c lt k v rt lta rta. lta \<and> rta \<and> bheight lt = bheight rt), rec_rbt True (\<lambda>c lt k v rt lta rta. lta \<and> rta \<and> bheight lt = bheight rt)) \<in> \<langle>Rk, Rv\<rangle>rbt_rel \<rightarrow> bool_rel
[PROOF STEP]
by (parametricity)


[STATEMENT]
lemma dual_downsets: "downsets = dual_ord.upsets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. downsets = ord.upsets (\<lambda>x y. y \<le> x)
[PROOF STEP]
by (simp add: dual_ord.dual_upsets)


[STATEMENT]
lemma convert_extTA_simps [simp]:
  "convert_extTA f \<epsilon> = \<epsilon>"
  "\<lbrace>convert_extTA f ta\<rbrace>\<^bsub>l\<^esub> = \<lbrace>ta\<rbrace>\<^bsub>l\<^esub>"
  "\<lbrace>convert_extTA f ta\<rbrace>\<^bsub>t\<^esub> = map (convert_new_thread_action f) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub>"
  "\<lbrace>convert_extTA f ta\<rbrace>\<^bsub>c\<^esub> = \<lbrace>ta\<rbrace>\<^bsub>c\<^esub>"
  "\<lbrace>convert_extTA f ta\<rbrace>\<^bsub>w\<^esub> = \<lbrace>ta\<rbrace>\<^bsub>w\<^esub>"
  "\<lbrace>convert_extTA f ta\<rbrace>\<^bsub>i\<^esub> = \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>"
  "convert_extTA f (las, tas, was, cas, is, obs) = (las, map (convert_new_thread_action f) tas, was, cas, is, obs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (convert_extTA f \<lbrace>\<rbrace> = \<lbrace>\<rbrace> &&& \<lbrace>convert_extTA f ta\<rbrace>\<^bsub>l\<^esub> = \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> &&& \<lbrace>convert_extTA f ta\<rbrace>\<^bsub>t\<^esub> = map (convert_new_thread_action f) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub>) &&& (\<lbrace>convert_extTA f ta\<rbrace>\<^bsub>c\<^esub> = \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> &&& \<lbrace>convert_extTA f ta\<rbrace>\<^bsub>w\<^esub> = \<lbrace>ta\<rbrace>\<^bsub>w\<^esub>) &&& \<lbrace>convert_extTA f ta\<rbrace>\<^bsub>i\<^esub> = \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> &&& convert_extTA f (las, tas, was, cas, is, obs) = (las, map (convert_new_thread_action f) tas, was, cas, is, obs)
[PROOF STEP]
apply(simp_all add: convert_extTA_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrace>(\<lbrace>ta\<rbrace>\<^bsub>l\<^esub>, map (convert_new_thread_action f) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub>, snd (snd ta))\<rbrace>\<^bsub>c\<^esub> = \<lbrace>ta\<rbrace>\<^bsub>c\<^esub>
 2. \<lbrace>(\<lbrace>ta\<rbrace>\<^bsub>l\<^esub>, map (convert_new_thread_action f) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub>, snd (snd ta))\<rbrace>\<^bsub>w\<^esub> = \<lbrace>ta\<rbrace>\<^bsub>w\<^esub>
 3. \<lbrace>(\<lbrace>ta\<rbrace>\<^bsub>l\<^esub>, map (convert_new_thread_action f) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub>, snd (snd ta))\<rbrace>\<^bsub>i\<^esub> = \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>
[PROOF STEP]
apply(cases ta, simp)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma finer_than_iff_nhds:
  "T1 finer_than T2 \<longleftrightarrow> (\<forall>X. openin T2 X \<longrightarrow> openin T1 (X \<inter> topspace T1)) \<and> (topspace T1 \<subseteq> topspace T2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (T1 finer_than T2) = ((\<forall>X. openin T2 X \<longrightarrow> openin T1 (X \<inter> topspace T1)) \<and> topspace T1 \<subseteq> topspace T2)
[PROOF STEP]
by (auto simp: finer_than_def continuous_map_alt)


[STATEMENT]
lemma (in filtrated_prob_space) AE_borel_eq:
fixes f::"'a\<Rightarrow>real"
assumes "f\<in> borel_measurable (F t)"
and "g\<in> borel_measurable (F t)"
and "AE w in M. f w = g w"
shows "{w\<in> space M. f w \<noteq> g w} \<in> sets (F t) \<and> emeasure M {w\<in> space M. f w \<noteq> g w} = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t) \<and> emeasure M {w \<in> space M. f w \<noteq> g w} = 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
 2. emeasure M {w \<in> space M. f w \<noteq> g w} = 0
[PROOF STEP]
show "{w \<in> space M. f w \<noteq> g w} \<in> sets (F t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
define minus where "minus = (\<lambda>w. (f w) - (g w))"
[PROOF STATE]
proof (state)
this:
minus = (\<lambda>w. f w - g w)

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
have "minus \<in> borel_measurable (F t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. minus \<in> borel_measurable (F t)
[PROOF STEP]
unfolding minus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>w. f w - g w) \<in> borel_measurable (F t)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable (F t)
g \<in> borel_measurable (F t)
AE w in M. f w = g w

goal (1 subgoal):
 1. (\<lambda>w. f w - g w) \<in> borel_measurable (F t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
minus \<in> borel_measurable (F t)

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
hence "{w\<in> space (F t). 0 < minus w} \<in> sets (F t)"
[PROOF STATE]
proof (prove)
using this:
minus \<in> borel_measurable (F t)

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<in> sets (F t)
[PROOF STEP]
using borel_measurable_iff_greater
[PROOF STATE]
proof (prove)
using this:
minus \<in> borel_measurable (F t)
(?f \<in> borel_measurable ?M) = (\<forall>a. {w \<in> space ?M. a < ?f w} \<in> sets ?M)

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<in> sets (F t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). 0 < minus w} \<in> sets (F t)

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). 0 < minus w} \<in> sets (F t)

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
have "{w\<in> space (F t). minus w < 0} \<in> sets (F t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space (F t). minus w < 0} \<in> sets (F t)
[PROOF STEP]
using borel_measurable_iff_less
      \<open>minus \<in> borel_measurable (F t)\<close>
[PROOF STATE]
proof (prove)
using this:
(?f \<in> borel_measurable ?M) = (\<forall>a. {w \<in> space ?M. ?f w < a} \<in> sets ?M)
minus \<in> borel_measurable (F t)

goal (1 subgoal):
 1. {w \<in> space (F t). minus w < 0} \<in> sets (F t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). minus w < 0} \<in> sets (F t)

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{w \<in> space (F t). 0 < minus w} \<in> sets (F t)
{w \<in> space (F t). minus w < 0} \<in> sets (F t)
[PROOF STEP]
have "{w\<in> space (F t). 0 < minus w} \<union> {w\<in> space (F t). minus w < 0} \<in> sets (F t)"
[PROOF STATE]
proof (prove)
using this:
{w \<in> space (F t). 0 < minus w} \<in> sets (F t)
{w \<in> space (F t). minus w < 0} \<in> sets (F t)

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<in> sets (F t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<in> sets (F t)

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<in> sets (F t)

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
have "{w\<in> space (F t). f w \<noteq> g w} = {w\<in> space (F t). 0 < minus w} \<union> {w\<in> space (F t). minus w < 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space (F t). f w \<noteq> g w} = {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {w \<in> space (F t). f w \<noteq> g w} \<subseteq> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
 2. {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
show "{w \<in> space (F t). f w \<noteq> g w} \<subseteq> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space (F t). f w \<noteq> g w} \<subseteq> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {w \<in> space (F t). f w \<noteq> g w} \<Longrightarrow> x \<in> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {w \<in> space (F t). f w \<noteq> g w} \<Longrightarrow> x \<in> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
[PROOF STEP]
assume "w \<in> {w \<in> space (F t). f w \<noteq> g w}"
[PROOF STATE]
proof (state)
this:
w \<in> {w \<in> space (F t). f w \<noteq> g w}

goal (1 subgoal):
 1. \<And>x. x \<in> {w \<in> space (F t). f w \<noteq> g w} \<Longrightarrow> x \<in> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
[PROOF STEP]
hence "w\<in> space (F t)" and "f w \<noteq> g w"
[PROOF STATE]
proof (prove)
using this:
w \<in> {w \<in> space (F t). f w \<noteq> g w}

goal (1 subgoal):
 1. w \<in> space (F t) &&& f w \<noteq> g w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> space (F t)
f w \<noteq> g w

goal (1 subgoal):
 1. \<And>x. x \<in> {w \<in> space (F t). f w \<noteq> g w} \<Longrightarrow> x \<in> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
[PROOF STEP]
thus "w\<in> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}"
[PROOF STATE]
proof (prove)
using this:
w \<in> space (F t)
f w \<noteq> g w

goal (1 subgoal):
 1. w \<in> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
[PROOF STEP]
unfolding minus_def
[PROOF STATE]
proof (prove)
using this:
w \<in> space (F t)
f w \<noteq> g w

goal (1 subgoal):
 1. w \<in> {w \<in> space (F t). 0 < f w - g w} \<union> {w \<in> space (F t). f w - g w < 0}
[PROOF STEP]
by (cases "f w < g w") auto
[PROOF STATE]
proof (state)
this:
w \<in> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). f w \<noteq> g w} \<subseteq> {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
have "{w \<in> space (F t). 0 < minus w} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
unfolding minus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space (F t). 0 < f w - g w} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). 0 < minus w} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). 0 < minus w} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
have "{w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
unfolding minus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w \<in> space (F t). f w - g w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{w \<in> space (F t). 0 < minus w} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
{w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
show "{w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}"
[PROOF STATE]
proof (prove)
using this:
{w \<in> space (F t). 0 < minus w} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
{w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}

goal (1 subgoal):
 1. {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<subseteq> {w \<in> space (F t). f w \<noteq> g w}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). f w \<noteq> g w} = {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{w \<in> space (F t). f w \<noteq> g w} = {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
have "space (F t) = space M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space (F t) = space M
[PROOF STEP]
using filtration
[PROOF STATE]
proof (prove)
using this:
Filtration.filtration M F

goal (1 subgoal):
 1. space (F t) = space M
[PROOF STEP]
unfolding filtration_def subalgebra_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>t. space (F t) = space M \<and> sets (F t) \<subseteq> events) \<and> (\<forall>s t. s \<le> t \<longrightarrow> space (F s) = space (F t) \<and> sets (F s) \<subseteq> sets (F t))

goal (1 subgoal):
 1. space (F t) = space M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
space (F t) = space M

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<in> sets (F t)
{w \<in> space (F t). f w \<noteq> g w} = {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
space (F t) = space M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0} \<in> sets (F t)
{w \<in> space (F t). f w \<noteq> g w} = {w \<in> space (F t). 0 < minus w} \<union> {w \<in> space (F t). minus w < 0}
space (F t) = space M

goal (1 subgoal):
 1. {w \<in> space M. f w \<noteq> g w} \<in> sets (F t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{w \<in> space M. f w \<noteq> g w} \<in> sets (F t)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{w \<in> space M. f w \<noteq> g w} \<in> sets (F t)

goal (1 subgoal):
 1. emeasure M {w \<in> space M. f w \<noteq> g w} = 0
[PROOF STEP]
show "emeasure M {w\<in> space M. f w \<noteq> g w} = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure M {w \<in> space M. f w \<noteq> g w} = 0
[PROOF STEP]
by (metis (no_types) AE_iff_measurable assms(3) emeasure_notin_sets)
[PROOF STATE]
proof (state)
this:
emeasure M {w \<in> space M. f w \<noteq> g w} = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trcl_empty_cons: "(c,[],c')\<in>trcl t \<Longrightarrow> (c=c')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c, [], c') \<in> trcl t \<Longrightarrow> c = c'
[PROOF STEP]
by (auto elim: trcl.cases)


[STATEMENT]
lemma reach_is_node: "\<lbrakk>reach trans p w q; is_node p; list_all is_alpha w\<rbrakk> \<Longrightarrow> is_node q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach trans p w q; is_node p; list_all is_alpha w\<rbrakk> \<Longrightarrow> is_node q
[PROOF STEP]
by (simp add: steps_is_node reach_def)


[STATEMENT]
lemma (in group) IDirProds_subgroup_id: "subgroup (S i) G \<Longrightarrow> IDirProds G S {i} = S i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup (S i) G \<Longrightarrow> IDirProds G S {i} = S i
[PROOF STEP]
by (simp add: generate_subgroup_id IDirProds_def)


[STATEMENT]
lemma finals_iff: "finals es \<longleftrightarrow> (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')"
  (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finals es = ((\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es'))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finals es \<Longrightarrow> (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')
 2. (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es') \<Longrightarrow> finals es
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
finals es

goal (2 subgoals):
 1. finals es \<Longrightarrow> (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')
 2. (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es') \<Longrightarrow> finals es
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
finals es

goal (1 subgoal):
 1. (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')
[PROOF STEP]
by induct(auto simp add: Cons_eq_append_conv Cons_eq_map_conv, metis)
[PROOF STATE]
proof (state)
this:
(\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')

goal (1 subgoal):
 1. (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es') \<Longrightarrow> finals es
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es') \<Longrightarrow> finals es
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
(\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')

goal (1 subgoal):
 1. (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es') \<Longrightarrow> finals es
[PROOF STEP]
thus ?lhs
[PROOF STATE]
proof (prove)
using this:
(\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')

goal (1 subgoal):
 1. finals es
[PROOF STEP]
by(induct es) auto
[PROOF STATE]
proof (state)
this:
finals es

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma remove_cycles_self:
  "x \<in> set xs \<Longrightarrow> remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys
[PROOF STEP]
assume x:"x \<in> set xs"
[PROOF STATE]
proof (state)
this:
x \<in> set xs

goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set xs
[PROOF STEP]
obtain ws where ws: "remove_cycles xs x ys = x # ws" "x \<notin> set ws"
[PROOF STATE]
proof (prove)
using this:
x \<in> set xs

goal (1 subgoal):
 1. (\<And>ws. \<lbrakk>remove_cycles xs x ys = x # ws; x \<notin> set ws\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using remove_cycles_begins_with[OF x, of ys]
[PROOF STATE]
proof (prove)
using this:
x \<in> set xs
\<exists>zs. remove_cycles xs x ys = x # zs \<and> x \<notin> set zs

goal (1 subgoal):
 1. (\<And>ws. \<lbrakk>remove_cycles xs x ys = x # ws; x \<notin> set ws\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
remove_cycles xs x ys = x # ws
x \<notin> set ws

goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys
[PROOF STEP]
from remove_cycles_id[OF this(2)]
[PROOF STATE]
proof (chain)
picking this:
remove_cycles ws x ?ys = rev ?ys @ ws
[PROOF STEP]
have "remove_cycles ws x [x] = x # ws"
[PROOF STATE]
proof (prove)
using this:
remove_cycles ws x ?ys = rev ?ys @ ws

goal (1 subgoal):
 1. remove_cycles ws x [x] = x # ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
remove_cycles ws x [x] = x # ws

goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys
[PROOF STEP]
with ws(1)
[PROOF STATE]
proof (chain)
picking this:
remove_cycles xs x ys = x # ws
remove_cycles ws x [x] = x # ws
[PROOF STEP]
show "remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys"
[PROOF STATE]
proof (prove)
using this:
remove_cycles xs x ys = x # ws
remove_cycles ws x [x] = x # ws

goal (1 subgoal):
 1. remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys

goal:
No subgoals!
[PROOF STEP]
qed