[STATEMENT]
lemma lift_to_metric_completion_isometry:
  fixes f::"('a::metric_space) \<Rightarrow> ('b::complete_space)"
  assumes "isometry_on UNIV f"
  shows "\<exists>g. isometry_on UNIV g
          \<and> range g = closure(range f)
          \<and> f = g o to_metric_completion
          \<and> (\<forall>x \<in> range to_metric_completion. g x = f (inv to_metric_completion x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
have *: "uniformly_continuous_on UNIV f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isUCont f
[PROOF STEP]
using assms isometry_on_uniformly_continuous
[PROOF STATE]
proof (prove)
using this:
isometry_on UNIV f
isometry_on ?X ?f \<Longrightarrow> uniformly_continuous_on ?X ?f

goal (1 subgoal):
 1. isUCont f
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
isUCont f

goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
obtain g where g: "uniformly_continuous_on UNIV g"
                    "f = g o to_metric_completion"
                    "\<And>x. x \<in> range to_metric_completion \<Longrightarrow> g x = f (inv to_metric_completion x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>isUCont g; f = g \<circ> to_metric_completion; \<And>x. x \<in> range to_metric_completion \<Longrightarrow> g x = f (inv to_metric_completion x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using lift_to_metric_completion[OF *]
[PROOF STATE]
proof (prove)
using this:
\<exists>g. isUCont g \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>isUCont g; f = g \<circ> to_metric_completion; \<And>x. x \<in> range to_metric_completion \<Longrightarrow> g x = f (inv to_metric_completion x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
isUCont g
f = g \<circ> to_metric_completion
?x \<in> range to_metric_completion \<Longrightarrow> g ?x = f (inv to_metric_completion ?x)

goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
have *: "isometry_on (range to_metric_completion) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on (range to_metric_completion) g
[PROOF STEP]
apply (rule isometry_on_cong[OF _ g(3)], rule isometry_on_compose[of _ _ f])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. isometry_on (range to_metric_completion) (inv to_metric_completion)
 2. isometry_on (inv to_metric_completion ` range to_metric_completion) f
 3. \<And>x. x \<in> range to_metric_completion \<Longrightarrow> x \<in> range to_metric_completion
[PROOF STEP]
using assms isometry_on_inverse[OF to_metric_completion_isometry] isometry_on_subset
[PROOF STATE]
proof (prove)
using this:
isometry_on UNIV f
isometry_on (range to_metric_completion) (inv to_metric_completion)
?x \<in> UNIV \<Longrightarrow> inv to_metric_completion (to_metric_completion ?x) = ?x
?y \<in> range to_metric_completion \<Longrightarrow> to_metric_completion (inv to_metric_completion ?y) = ?y
bij_betw to_metric_completion UNIV (range to_metric_completion)
\<lbrakk>isometry_on ?X ?f; ?Y \<subseteq> ?X\<rbrakk> \<Longrightarrow> isometry_on ?Y ?f

goal (3 subgoals):
 1. isometry_on (range to_metric_completion) (inv to_metric_completion)
 2. isometry_on (inv to_metric_completion ` range to_metric_completion) f
 3. \<And>x. x \<in> range to_metric_completion \<Longrightarrow> x \<in> range to_metric_completion
[PROOF STEP]
by (auto) (fastforce)
[PROOF STATE]
proof (state)
this:
isometry_on (range to_metric_completion) g

goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
isometry_on (range to_metric_completion) g
[PROOF STEP]
have "isometry_on UNIV g"
[PROOF STATE]
proof (prove)
using this:
isometry_on (range to_metric_completion) g

goal (1 subgoal):
 1. isometry_on UNIV g
[PROOF STEP]
unfolding to_metric_completion_dense'[symmetric]
[PROOF STATE]
proof (prove)
using this:
isometry_on (range to_metric_completion) g

goal (1 subgoal):
 1. isometry_on (closure (range to_metric_completion)) g
[PROOF STEP]
apply (rule isometry_on_closure)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on (closure (range to_metric_completion)) g
[PROOF STEP]
using continuous_on_subset[OF uniformly_continuous_imp_continuous[OF g(1)]]
[PROOF STATE]
proof (prove)
using this:
?t \<subseteq> UNIV \<Longrightarrow> continuous_on ?t g

goal (1 subgoal):
 1. continuous_on (closure (range to_metric_completion)) g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isometry_on UNIV g

goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
have "g`(range to_metric_completion) \<subseteq> range f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g ` range to_metric_completion \<subseteq> range f
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
isUCont g
f = g \<circ> to_metric_completion
?x \<in> range to_metric_completion \<Longrightarrow> g ?x = f (inv to_metric_completion ?x)

goal (1 subgoal):
 1. g ` range to_metric_completion \<subseteq> range f
[PROOF STEP]
unfolding comp_def
[PROOF STATE]
proof (prove)
using this:
isUCont g
f = (\<lambda>x. g (to_metric_completion x))
?x \<in> range to_metric_completion \<Longrightarrow> g ?x = f (inv to_metric_completion ?x)

goal (1 subgoal):
 1. g ` range to_metric_completion \<subseteq> range f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g ` range to_metric_completion \<subseteq> range f

goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g ` range to_metric_completion \<subseteq> range f

goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
have "g`(closure (range to_metric_completion)) \<subseteq> closure (g`(range to_metric_completion))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g ` closure (range to_metric_completion) \<subseteq> closure (g ` range to_metric_completion)
[PROOF STEP]
using uniformly_continuous_imp_continuous[OF g(1)]
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV g

goal (1 subgoal):
 1. g ` closure (range to_metric_completion) \<subseteq> closure (g ` range to_metric_completion)
[PROOF STEP]
by (meson closed_closure closure_subset continuous_on_subset image_closure_subset top_greatest)
[PROOF STATE]
proof (state)
this:
g ` closure (range to_metric_completion) \<subseteq> closure (g ` range to_metric_completion)

goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
g ` range to_metric_completion \<subseteq> range f
g ` closure (range to_metric_completion) \<subseteq> closure (g ` range to_metric_completion)
[PROOF STEP]
have "range g \<subseteq> closure (range f)"
[PROOF STATE]
proof (prove)
using this:
g ` range to_metric_completion \<subseteq> range f
g ` closure (range to_metric_completion) \<subseteq> closure (g ` range to_metric_completion)

goal (1 subgoal):
 1. range g \<subseteq> closure (range f)
[PROOF STEP]
unfolding to_metric_completion_dense'
[PROOF STATE]
proof (prove)
using this:
g ` range to_metric_completion \<subseteq> range f
range g \<subseteq> closure (g ` range to_metric_completion)

goal (1 subgoal):
 1. range g \<subseteq> closure (range f)
[PROOF STEP]
by (simp add: g(2) image_comp)
[PROOF STATE]
proof (state)
this:
range g \<subseteq> closure (range f)

goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
have "range f \<subseteq> range g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range f \<subseteq> range g
[PROOF STEP]
using g(2)
[PROOF STATE]
proof (prove)
using this:
f = g \<circ> to_metric_completion

goal (1 subgoal):
 1. range f \<subseteq> range g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
range f \<subseteq> range g

goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
range f \<subseteq> range g

goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
have "closed (range g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (range g)
[PROOF STEP]
using isometry_on_complete_image[OF \<open>isometry_on UNIV g\<close>]
[PROOF STATE]
proof (prove)
using this:
complete UNIV \<Longrightarrow> complete (range g)

goal (1 subgoal):
 1. closed (range g)
[PROOF STEP]
by (simp add: complete_eq_closed)
[PROOF STATE]
proof (state)
this:
closed (range g)

goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
range f \<subseteq> range g
closed (range g)
[PROOF STEP]
have "closure (range f) \<subseteq> range g"
[PROOF STATE]
proof (prove)
using this:
range f \<subseteq> range g
closed (range g)

goal (1 subgoal):
 1. closure (range f) \<subseteq> range g
[PROOF STEP]
by (simp add: closure_minimal)
[PROOF STATE]
proof (state)
this:
closure (range f) \<subseteq> range g

goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closure (range f) \<subseteq> range g
[PROOF STEP]
have "range g = closure (range f)"
[PROOF STATE]
proof (prove)
using this:
closure (range f) \<subseteq> range g

goal (1 subgoal):
 1. range g = closure (range f)
[PROOF STEP]
using \<open>range g \<subseteq> closure (range f)\<close>
[PROOF STATE]
proof (prove)
using this:
closure (range f) \<subseteq> range g
range g \<subseteq> closure (range f)

goal (1 subgoal):
 1. range g = closure (range f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
range g = closure (range f)

goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
range g = closure (range f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
range g = closure (range f)

goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
using \<open>isometry_on UNIV g\<close> g
[PROOF STATE]
proof (prove)
using this:
range g = closure (range f)
isometry_on UNIV g
isUCont g
f = g \<circ> to_metric_completion
?x \<in> range to_metric_completion \<Longrightarrow> g ?x = f (inv to_metric_completion ?x)

goal (1 subgoal):
 1. \<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>g. isometry_on UNIV g \<and> range g = closure (range f) \<and> f = g \<circ> to_metric_completion \<and> (\<forall>x\<in>range to_metric_completion. g x = f (inv to_metric_completion x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma second_countable_iff_dense_countable_subset:
  "(\<exists>B::'a::metric_space set set. countable B \<and> topological_basis B)
    \<longleftrightarrow> (\<exists>A::'a set. countable A \<and> closure A = UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>B. countable B \<and> topological_basis B) = (\<exists>A. countable A \<and> closure A = UNIV)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>B. countable B \<and> topological_basis B \<Longrightarrow> \<exists>A. countable A \<and> closure A = UNIV
 2. \<exists>A. countable A \<and> closure A = UNIV \<Longrightarrow> \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
assume "\<exists>B::'a set set. countable B \<and> topological_basis B"
[PROOF STATE]
proof (state)
this:
\<exists>B. countable B \<and> topological_basis B

goal (2 subgoals):
 1. \<exists>B. countable B \<and> topological_basis B \<Longrightarrow> \<exists>A. countable A \<and> closure A = UNIV
 2. \<exists>A. countable A \<and> closure A = UNIV \<Longrightarrow> \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
obtain B::"'a set set" where "countable B" "topological_basis B"
[PROOF STATE]
proof (prove)
using this:
\<exists>B. countable B \<and> topological_basis B

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>countable B; topological_basis B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
countable B
topological_basis B

goal (2 subgoals):
 1. \<exists>B. countable B \<and> topological_basis B \<Longrightarrow> \<exists>A. countable A \<and> closure A = UNIV
 2. \<exists>A. countable A \<and> closure A = UNIV \<Longrightarrow> \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
define A where "A = (\<lambda>U. SOME x. x \<in> U)`B"
[PROOF STATE]
proof (state)
this:
A = (\<lambda>U. SOME x. x \<in> U) ` B

goal (2 subgoals):
 1. \<exists>B. countable B \<and> topological_basis B \<Longrightarrow> \<exists>A. countable A \<and> closure A = UNIV
 2. \<exists>A. countable A \<and> closure A = UNIV \<Longrightarrow> \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
have "countable A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable A
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable ((\<lambda>U. SOME x. x \<in> U) ` B)
[PROOF STEP]
using \<open>countable B\<close>
[PROOF STATE]
proof (prove)
using this:
countable B

goal (1 subgoal):
 1. countable ((\<lambda>U. SOME x. x \<in> U) ` B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
countable A

goal (2 subgoals):
 1. \<exists>B. countable B \<and> topological_basis B \<Longrightarrow> \<exists>A. countable A \<and> closure A = UNIV
 2. \<exists>A. countable A \<and> closure A = UNIV \<Longrightarrow> \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
countable A

goal (2 subgoals):
 1. \<exists>B. countable B \<and> topological_basis B \<Longrightarrow> \<exists>A. countable A \<and> closure A = UNIV
 2. \<exists>A. countable A \<and> closure A = UNIV \<Longrightarrow> \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
have "closure A = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure A = UNIV
[PROOF STEP]
proof (auto simp add: closure_approachable)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x e. 0 < e \<Longrightarrow> \<exists>y\<in>A. dist y x < e
[PROOF STEP]
fix x::'a and e::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x e. 0 < e \<Longrightarrow> \<exists>y\<in>A. dist y x < e
[PROOF STEP]
assume "e > 0"
[PROOF STATE]
proof (state)
this:
0 < e

goal (1 subgoal):
 1. \<And>x e. 0 < e \<Longrightarrow> \<exists>y\<in>A. dist y x < e
[PROOF STEP]
obtain U where "U \<in> B" "x \<in> U" "U \<subseteq> ball x e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>U. \<lbrakk>U \<in> B; x \<in> U; U \<subseteq> ball x e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule topological_basisE[OF \<open>topological_basis B\<close>, of "ball x e" x], auto simp add: \<open>e > 0\<close>)
[PROOF STATE]
proof (state)
this:
U \<in> B
x \<in> U
U \<subseteq> ball x e

goal (1 subgoal):
 1. \<And>x e. 0 < e \<Longrightarrow> \<exists>y\<in>A. dist y x < e
[PROOF STEP]
define y where "y = (\<lambda>U. SOME x. x \<in> U) U"
[PROOF STATE]
proof (state)
this:
y = (SOME x. x \<in> U)

goal (1 subgoal):
 1. \<And>x e. 0 < e \<Longrightarrow> \<exists>y\<in>A. dist y x < e
[PROOF STEP]
have "y \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> U
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME x. x \<in> U) \<in> U
[PROOF STEP]
using \<open>x \<in> U\<close> some_in_eq
[PROOF STATE]
proof (prove)
using this:
x \<in> U
((SOME x. x \<in> ?A) \<in> ?A) = (?A \<noteq> {})

goal (1 subgoal):
 1. (SOME x. x \<in> U) \<in> U
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
y \<in> U

goal (1 subgoal):
 1. \<And>x e. 0 < e \<Longrightarrow> \<exists>y\<in>A. dist y x < e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> U
[PROOF STEP]
have "dist y x < e"
[PROOF STATE]
proof (prove)
using this:
y \<in> U

goal (1 subgoal):
 1. dist y x < e
[PROOF STEP]
using \<open>U \<subseteq> ball x e\<close>
[PROOF STATE]
proof (prove)
using this:
y \<in> U
U \<subseteq> ball x e

goal (1 subgoal):
 1. dist y x < e
[PROOF STEP]
by (metis dist_commute mem_ball subset_iff)
[PROOF STATE]
proof (state)
this:
dist y x < e

goal (1 subgoal):
 1. \<And>x e. 0 < e \<Longrightarrow> \<exists>y\<in>A. dist y x < e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dist y x < e

goal (1 subgoal):
 1. \<And>x e. 0 < e \<Longrightarrow> \<exists>y\<in>A. dist y x < e
[PROOF STEP]
have "y \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> A
[PROOF STEP]
unfolding A_def y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME x. x \<in> U) \<in> (\<lambda>U. SOME x. x \<in> U) ` B
[PROOF STEP]
using \<open>U \<in> B\<close>
[PROOF STATE]
proof (prove)
using this:
U \<in> B

goal (1 subgoal):
 1. (SOME x. x \<in> U) \<in> (\<lambda>U. SOME x. x \<in> U) ` B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> A

goal (1 subgoal):
 1. \<And>x e. 0 < e \<Longrightarrow> \<exists>y\<in>A. dist y x < e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dist y x < e
y \<in> A
[PROOF STEP]
show "\<exists>y\<in>A. dist y x < e"
[PROOF STATE]
proof (prove)
using this:
dist y x < e
y \<in> A

goal (1 subgoal):
 1. \<exists>y\<in>A. dist y x < e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>A. dist y x < e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
closure A = UNIV

goal (2 subgoals):
 1. \<exists>B. countable B \<and> topological_basis B \<Longrightarrow> \<exists>A. countable A \<and> closure A = UNIV
 2. \<exists>A. countable A \<and> closure A = UNIV \<Longrightarrow> \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
countable A
closure A = UNIV
[PROOF STEP]
show "\<exists>A::'a set. countable A \<and> closure A = UNIV"
[PROOF STATE]
proof (prove)
using this:
countable A
closure A = UNIV

goal (1 subgoal):
 1. \<exists>A. countable A \<and> closure A = UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>A. countable A \<and> closure A = UNIV

goal (1 subgoal):
 1. \<exists>A. countable A \<and> closure A = UNIV \<Longrightarrow> \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A. countable A \<and> closure A = UNIV \<Longrightarrow> \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
assume "\<exists>A::'a set. countable A \<and> closure A = UNIV"
[PROOF STATE]
proof (state)
this:
\<exists>A. countable A \<and> closure A = UNIV

goal (1 subgoal):
 1. \<exists>A. countable A \<and> closure A = UNIV \<Longrightarrow> \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>A. countable A \<and> closure A = UNIV
[PROOF STEP]
obtain A::"'a set" where "countable A" "closure A = UNIV"
[PROOF STATE]
proof (prove)
using this:
\<exists>A. countable A \<and> closure A = UNIV

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>countable A; closure A = UNIV\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
countable A
closure A = UNIV

goal (1 subgoal):
 1. \<exists>A. countable A \<and> closure A = UNIV \<Longrightarrow> \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
define B where "B = (\<lambda>(x, (n::nat)). ball x (1/n))`(A \<times> UNIV)"
[PROOF STATE]
proof (state)
this:
B = (\<lambda>(xa, x). ball xa (1 / real x)) ` (A \<times> UNIV)

goal (1 subgoal):
 1. \<exists>A. countable A \<and> closure A = UNIV \<Longrightarrow> \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
have "countable B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable B
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable ((\<lambda>(xa, x). ball xa (1 / real x)) ` (A \<times> UNIV))
[PROOF STEP]
using \<open>countable A\<close>
[PROOF STATE]
proof (prove)
using this:
countable A

goal (1 subgoal):
 1. countable ((\<lambda>(xa, x). ball xa (1 / real x)) ` (A \<times> UNIV))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
countable B

goal (1 subgoal):
 1. \<exists>A. countable A \<and> closure A = UNIV \<Longrightarrow> \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
countable B

goal (1 subgoal):
 1. \<exists>A. countable A \<and> closure A = UNIV \<Longrightarrow> \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
have "topological_basis B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. topological_basis B
[PROOF STEP]
proof (rule topological_basisI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>B'. B' \<in> B \<Longrightarrow> open B'
 2. \<And>O' x. \<lbrakk>open O'; x \<in> O'\<rbrakk> \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'
[PROOF STEP]
fix x::'a and U
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>B'. B' \<in> B \<Longrightarrow> open B'
 2. \<And>O' x. \<lbrakk>open O'; x \<in> O'\<rbrakk> \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'
[PROOF STEP]
assume "x \<in> U" "open U"
[PROOF STATE]
proof (state)
this:
x \<in> U
open U

goal (2 subgoals):
 1. \<And>B'. B' \<in> B \<Longrightarrow> open B'
 2. \<And>O' x. \<lbrakk>open O'; x \<in> O'\<rbrakk> \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> U
open U
[PROOF STEP]
obtain e where "e > 0" "ball x e \<subseteq> U"
[PROOF STATE]
proof (prove)
using this:
x \<in> U
open U

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>0 < e; ball x e \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using openE
[PROOF STATE]
proof (prove)
using this:
x \<in> U
open U
\<lbrakk>open ?S; ?x \<in> ?S; \<And>e. \<lbrakk>0 < e; ball ?x e \<subseteq> ?S\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>0 < e; ball x e \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < e
ball x e \<subseteq> U

goal (2 subgoals):
 1. \<And>B'. B' \<in> B \<Longrightarrow> open B'
 2. \<And>O' x. \<lbrakk>open O'; x \<in> O'\<rbrakk> \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'
[PROOF STEP]
obtain n::nat where "n > 2/e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. 2 / e < real n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reals_Archimedean2
[PROOF STATE]
proof (prove)
using this:
\<exists>n. ?x < of_nat n

goal (1 subgoal):
 1. (\<And>n. 2 / e < real n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 / e < real n

goal (2 subgoals):
 1. \<And>B'. B' \<in> B \<Longrightarrow> open B'
 2. \<And>O' x. \<lbrakk>open O'; x \<in> O'\<rbrakk> \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 / e < real n
[PROOF STEP]
have "n > 0"
[PROOF STATE]
proof (prove)
using this:
2 / e < real n

goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
using \<open>e > 0\<close> not_less
[PROOF STATE]
proof (prove)
using this:
2 / e < real n
0 < e
(\<not> ?x < ?y) = (?y \<le> ?x)

goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
0 < n

goal (2 subgoals):
 1. \<And>B'. B' \<in> B \<Longrightarrow> open B'
 2. \<And>O' x. \<lbrakk>open O'; x \<in> O'\<rbrakk> \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
have "1/n > 0"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. 0 < 1 / real n
[PROOF STEP]
using zero_less_divide_iff
[PROOF STATE]
proof (prove)
using this:
0 < n
((0::?'a) < ?a / ?b) = ((0::?'a) < ?a \<and> (0::?'a) < ?b \<or> ?a < (0::?'a) \<and> ?b < (0::?'a))

goal (1 subgoal):
 1. 0 < 1 / real n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
0 < 1 / real n

goal (2 subgoals):
 1. \<And>B'. B' \<in> B \<Longrightarrow> open B'
 2. \<And>O' x. \<lbrakk>open O'; x \<in> O'\<rbrakk> \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < 1 / real n
[PROOF STEP]
obtain y where y: "y \<in> A" "dist x y < 1/n"
[PROOF STATE]
proof (prove)
using this:
0 < 1 / real n

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> A; dist x y < 1 / real n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis \<open>closure A = UNIV\<close> UNIV_I closure_approachable dist_commute)
[PROOF STATE]
proof (state)
this:
y \<in> A
dist x y < 1 / real n

goal (2 subgoals):
 1. \<And>B'. B' \<in> B \<Longrightarrow> open B'
 2. \<And>O' x. \<lbrakk>open O'; x \<in> O'\<rbrakk> \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> A
dist x y < 1 / real n
[PROOF STEP]
have "ball y (1/n) \<in> B"
[PROOF STATE]
proof (prove)
using this:
y \<in> A
dist x y < 1 / real n

goal (1 subgoal):
 1. ball y (1 / real n) \<in> B
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
y \<in> A
dist x y < 1 / real n

goal (1 subgoal):
 1. ball y (1 / real n) \<in> (\<lambda>(xa, x). ball xa (1 / real x)) ` (A \<times> UNIV)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ball y (1 / real n) \<in> B

goal (2 subgoals):
 1. \<And>B'. B' \<in> B \<Longrightarrow> open B'
 2. \<And>O' x. \<lbrakk>open O'; x \<in> O'\<rbrakk> \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ball y (1 / real n) \<in> B

goal (2 subgoals):
 1. \<And>B'. B' \<in> B \<Longrightarrow> open B'
 2. \<And>O' x. \<lbrakk>open O'; x \<in> O'\<rbrakk> \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'
[PROOF STEP]
have "x \<in> ball y (1/n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> ball y (1 / real n)
[PROOF STEP]
using y(2)
[PROOF STATE]
proof (prove)
using this:
dist x y < 1 / real n

goal (1 subgoal):
 1. x \<in> ball y (1 / real n)
[PROOF STEP]
by (auto simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
x \<in> ball y (1 / real n)

goal (2 subgoals):
 1. \<And>B'. B' \<in> B \<Longrightarrow> open B'
 2. \<And>O' x. \<lbrakk>open O'; x \<in> O'\<rbrakk> \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> ball y (1 / real n)

goal (2 subgoals):
 1. \<And>B'. B' \<in> B \<Longrightarrow> open B'
 2. \<And>O' x. \<lbrakk>open O'; x \<in> O'\<rbrakk> \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'
[PROOF STEP]
have "ball y (1/n) \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ball y (1 / real n) \<subseteq> U
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. dist y x < 1 / real n \<Longrightarrow> x \<in> U
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. dist y x < 1 / real n \<Longrightarrow> x \<in> U
[PROOF STEP]
assume z: "dist y z < 1/n"
[PROOF STATE]
proof (state)
this:
dist y z < 1 / real n

goal (1 subgoal):
 1. \<And>x. dist y x < 1 / real n \<Longrightarrow> x \<in> U
[PROOF STEP]
have "dist z x \<le> dist z y + dist y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist z x \<le> dist z y + dist y x
[PROOF STEP]
using dist_triangle
[PROOF STATE]
proof (prove)
using this:
dist ?x ?z \<le> dist ?x ?y + dist ?y ?z

goal (1 subgoal):
 1. dist z x \<le> dist z y + dist y x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist z x \<le> dist z y + dist y x

goal (1 subgoal):
 1. \<And>x. dist y x < 1 / real n \<Longrightarrow> x \<in> U
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist z x \<le> dist z y + dist y x

goal (1 subgoal):
 1. \<And>x. dist y x < 1 / real n \<Longrightarrow> x \<in> U
[PROOF STEP]
have "... < 1/n + 1/n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist z y + dist y x < 1 / real n + 1 / real n
[PROOF STEP]
using z y(2)
[PROOF STATE]
proof (prove)
using this:
dist y z < 1 / real n
dist x y < 1 / real n

goal (1 subgoal):
 1. dist z y + dist y x < 1 / real n + 1 / real n
[PROOF STEP]
by (auto simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist z y + dist y x < 1 / real n + 1 / real n

goal (1 subgoal):
 1. \<And>x. dist y x < 1 / real n \<Longrightarrow> x \<in> U
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist z y + dist y x < 1 / real n + 1 / real n

goal (1 subgoal):
 1. \<And>x. dist y x < 1 / real n \<Longrightarrow> x \<in> U
[PROOF STEP]
have "... < e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / real n + 1 / real n < e
[PROOF STEP]
using \<open>n > 2/e\<close> \<open>e > 0\<close> \<open>n > 0\<close>
[PROOF STATE]
proof (prove)
using this:
2 / e < real n
0 < e
0 < n

goal (1 subgoal):
 1. 1 / real n + 1 / real n < e
[PROOF STEP]
by (auto simp add: divide_simps mult.commute)
[PROOF STATE]
proof (state)
this:
1 / real n + 1 / real n < e

goal (1 subgoal):
 1. \<And>x. dist y x < 1 / real n \<Longrightarrow> x \<in> U
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist z x < e
[PROOF STEP]
have "z \<in> ball x e"
[PROOF STATE]
proof (prove)
using this:
dist z x < e

goal (1 subgoal):
 1. z \<in> ball x e
[PROOF STEP]
by (auto simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
z \<in> ball x e

goal (1 subgoal):
 1. \<And>x. dist y x < 1 / real n \<Longrightarrow> x \<in> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> ball x e
[PROOF STEP]
show "z \<in> U"
[PROOF STATE]
proof (prove)
using this:
z \<in> ball x e

goal (1 subgoal):
 1. z \<in> U
[PROOF STEP]
using \<open>ball x e \<subseteq> U\<close>
[PROOF STATE]
proof (prove)
using this:
z \<in> ball x e
ball x e \<subseteq> U

goal (1 subgoal):
 1. z \<in> U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> U

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ball y (1 / real n) \<subseteq> U

goal (2 subgoals):
 1. \<And>B'. B' \<in> B \<Longrightarrow> open B'
 2. \<And>O' x. \<lbrakk>open O'; x \<in> O'\<rbrakk> \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ball y (1 / real n) \<in> B
x \<in> ball y (1 / real n)
ball y (1 / real n) \<subseteq> U
[PROOF STEP]
show "\<exists>V\<in>B. x \<in> V \<and> V \<subseteq> U"
[PROOF STATE]
proof (prove)
using this:
ball y (1 / real n) \<in> B
x \<in> ball y (1 / real n)
ball y (1 / real n) \<subseteq> U

goal (1 subgoal):
 1. \<exists>V\<in>B. x \<in> V \<and> V \<subseteq> U
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>V\<in>B. x \<in> V \<and> V \<subseteq> U

goal (1 subgoal):
 1. \<And>B'. B' \<in> B \<Longrightarrow> open B'
[PROOF STEP]
qed (auto simp add: B_def)
[PROOF STATE]
proof (state)
this:
topological_basis B

goal (1 subgoal):
 1. \<exists>A. countable A \<and> closure A = UNIV \<Longrightarrow> \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
countable B
topological_basis B
[PROOF STEP]
show "\<exists>B::'a set set. countable B \<and> topological_basis B"
[PROOF STATE]
proof (prove)
using this:
countable B
topological_basis B

goal (1 subgoal):
 1. \<exists>B. countable B \<and> topological_basis B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>B. countable B \<and> topological_basis B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma second_countable_metric_dense_subset:
  "\<exists>A::'a::{metric_space, second_countable_topology} set. countable A \<and> closure A = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. countable A \<and> closure A = UNIV
[PROOF STEP]
using ex_countable_basis
[PROOF STATE]
proof (prove)
using this:
\<exists>B. countable B \<and> topological_basis B

goal (1 subgoal):
 1. \<exists>A. countable A \<and> closure A = UNIV
[PROOF STEP]
by (auto simp add: second_countable_iff_dense_countable_subset[symmetric])


[STATEMENT]
lemma length_merge [simp]:
  "length (merge xs ys) = length xs + length ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (local.merge xs ys) = length xs + length ys
[PROOF STEP]
by (induct xs ys rule: merge.induct) simp_all


[STATEMENT]
lemma length_merge_pairs [simp]:
  "length (merge_pairs xs) = (1 + length xs) div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (local.merge_pairs xs) = (1 + length xs) div 2
[PROOF STEP]
by (induct xs rule: merge_pairs.induct) simp_all


[STATEMENT]
lemma ascP_Cons [simp]: "ascP ((#) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ascP ((#) x)
[PROOF STEP]
by (simp add: ascP_def)


[STATEMENT]
lemma ascP_comp_append_Cons [simp]:
  "ascP (\<lambda>xs. f [] @ x # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ascP (\<lambda>xs. f [] @ x # xs)
[PROOF STEP]
by (auto simp: ascP_def)


[STATEMENT]
lemma ascP_f_Cons:
  assumes "ascP f"
  shows "f (x # xs) = f [] @ x # xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (x # xs) = f [] @ x # xs
[PROOF STEP]
using \<open>ascP f\<close> [unfolded ascP_def, THEN spec, of "x # xs"]
[PROOF STATE]
proof (prove)
using this:
f (x # xs) = f [] @ x # xs

goal (1 subgoal):
 1. f (x # xs) = f [] @ x # xs
[PROOF STEP]
.


[STATEMENT]
lemma ascP_comp_Cons [simp]:
  assumes "ascP f"
  shows "ascP (\<lambda>ys. f (x # ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ascP (\<lambda>ys. f (x # ys))
[PROOF STEP]
proof (unfold ascP_def, intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. f (x # xs) = f [x] @ xs
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. f (x # xs) = f [x] @ xs
[PROOF STEP]
show "f (x # xs) = f [x] @ xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (x # xs) = f [x] @ xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ascP f

goal (1 subgoal):
 1. f (x # xs) = f [x] @ xs
[PROOF STEP]
by (simp add: ascP_f_Cons)
[PROOF STATE]
proof (state)
this:
f (x # xs) = f [x] @ xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ascP_f_singleton:
  assumes "ascP f"
  shows "f [x] = f [] @ [x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f [x] = f [] @ [x]
[PROOF STEP]
by (rule ascP_f_Cons [OF assms])


[STATEMENT]
lemma length_concat_merge_pairs [simp]:
  "length (concat (merge_pairs xss)) = length (concat xss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (concat (local.merge_pairs xss)) = length (concat xss)
[PROOF STEP]
by (induct xss rule: merge_pairs.induct) simp_all


[STATEMENT]
lemma mset_merge [simp]:
  "mset (merge xs ys) = mset xs + mset ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (local.merge xs ys) = mset xs + mset ys
[PROOF STEP]
by (induct xs ys rule: merge.induct) simp_all


[STATEMENT]
lemma set_merge [simp]:
  "set (merge xs ys) = set xs \<union> set ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (local.merge xs ys) = set xs \<union> set ys
[PROOF STEP]
by (simp flip: set_mset_mset)


[STATEMENT]
lemma mset_concat_merge_pairs [simp]:
  "mset (concat (merge_pairs xs)) = mset (concat xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (concat (local.merge_pairs xs)) = mset (concat xs)
[PROOF STEP]
by (induct xs rule: merge_pairs.induct) auto


[STATEMENT]
lemma set_concat_merge_pairs [simp]:
  "set (concat (merge_pairs xs)) = set (concat xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (concat (local.merge_pairs xs)) = set (concat xs)
[PROOF STEP]
by (simp flip: set_mset_mset)


[STATEMENT]
lemma mset_merge_all [simp]:
  "mset (merge_all xs) = mset (concat xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (local.merge_all xs) = mset (concat xs)
[PROOF STEP]
by (induct xs rule: merge_all.induct) simp_all


[STATEMENT]
lemma set_merge_all [simp]:
  "set (merge_all xs) = set (concat xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (local.merge_all xs) = set (concat xs)
[PROOF STEP]
by (simp flip: set_mset_mset)


[STATEMENT]
lemma mset_msort_key:
  "mset (msort_key xs) = mset xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (local.msort_key xs) = mset xs
[PROOF STEP]
by (auto)


[STATEMENT]
lemma sorted_merge [simp]:
  assumes "sorted (map key xs)" and "sorted (map key ys)"
  shows "sorted (map key (merge xs ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (map key (local.merge xs ys))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sorted (map key xs)
sorted (map key ys)

goal (1 subgoal):
 1. sorted (map key (local.merge xs ys))
[PROOF STEP]
by (induct xs ys rule: merge.induct) (auto)


[STATEMENT]
lemma sorted_merge_pairs [simp]:
  assumes "\<forall>x\<in>set xs. sorted (map key x)"
  shows "\<forall>x\<in>set (merge_pairs xs). sorted (map key x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (local.merge_pairs xs). sorted (map key x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set xs. sorted (map key x)

goal (1 subgoal):
 1. \<forall>x\<in>set (local.merge_pairs xs). sorted (map key x)
[PROOF STEP]
by (induct xs rule: merge_pairs.induct) simp_all


[STATEMENT]
lemma sorted_merge_all:
  assumes "\<forall>x\<in>set xs. sorted (map key x)"
  shows "sorted (map key (merge_all xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (map key (local.merge_all xs))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set xs. sorted (map key x)

goal (1 subgoal):
 1. sorted (map key (local.merge_all xs))
[PROOF STEP]
by (induct xs rule: merge_all.induct) simp_all


[STATEMENT]
lemma sorted_msort_key:
  "sorted (map key (msort_key xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (map key (local.msort_key xs))
[PROOF STEP]
by (unfold msort_key.simps) (intro sorted_merge_all sorted_sequences)


[STATEMENT]
lemma filter_by_key_merge_is_append [simp]:
  assumes "sorted (map key xs)"
  shows "[y\<leftarrow>merge xs ys. key y = k] = [y\<leftarrow>xs. key y = k] @ [y\<leftarrow>ys. key y = k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>y. key y = k) (local.merge xs ys) = filter (\<lambda>y. key y = k) xs @ filter (\<lambda>y. key y = k) ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sorted (map key xs)

goal (1 subgoal):
 1. filter (\<lambda>y. key y = k) (local.merge xs ys) = filter (\<lambda>y. key y = k) xs @ filter (\<lambda>y. key y = k) ys
[PROOF STEP]
by (induct xs ys rule: merge.induct) (auto simp: Cons_eq_append_conv leD intro!: filter_False)


[STATEMENT]
lemma filter_by_key_merge_pairs [simp]:
  assumes "\<forall>xs\<in>set xss. sorted (map key xs)"
  shows "[y\<leftarrow>concat (merge_pairs xss). key y = k] = [y\<leftarrow>concat xss. key y = k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>y. key y = k) (concat (local.merge_pairs xss)) = filter (\<lambda>y. key y = k) (concat xss)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>xs\<in>set xss. sorted (map key xs)

goal (1 subgoal):
 1. filter (\<lambda>y. key y = k) (concat (local.merge_pairs xss)) = filter (\<lambda>y. key y = k) (concat xss)
[PROOF STEP]
by (induct xss rule: merge_pairs.induct) simp_all


[STATEMENT]
lemma filter_by_key_merge_all [simp]:
  assumes "\<forall>xs\<in>set xss. sorted (map key xs)"
  shows "[y\<leftarrow>merge_all xss. key y = k] = [y\<leftarrow>concat xss. key y = k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>y. key y = k) (local.merge_all xss) = filter (\<lambda>y. key y = k) (concat xss)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>xs\<in>set xss. sorted (map key xs)

goal (1 subgoal):
 1. filter (\<lambda>y. key y = k) (local.merge_all xss) = filter (\<lambda>y. key y = k) (concat xss)
[PROOF STEP]
by (induct xss rule: merge_all.induct) simp_all


[STATEMENT]
lemma filter_by_key_merge_all_sequences [simp]:
  "[x\<leftarrow>merge_all (sequences xs) . key x = k] = [x\<leftarrow>xs . key x = k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>x. key x = k) (local.merge_all (local.sequences xs)) = filter (\<lambda>x. key x = k) xs
[PROOF STEP]
using sorted_sequences [of xs]
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (local.sequences xs). sorted (map key x)

goal (1 subgoal):
 1. filter (\<lambda>x. key x = k) (local.merge_all (local.sequences xs)) = filter (\<lambda>x. key x = k) xs
[PROOF STEP]
by simp


[STATEMENT]
lemma msort_key_stable:
  "[x\<leftarrow>msort_key xs. key x = k] = [x\<leftarrow>xs. key x = k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>x. key x = k) (local.msort_key xs) = filter (\<lambda>x. key x = k) xs
[PROOF STEP]
by auto


[STATEMENT]
lemma sort_key_msort_key_conv:
  "sort_key key = msort_key"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sort_key key = local.msort_key
[PROOF STEP]
using msort_key_stable [of "key x" for x]
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>x. key x = key ?x3) (local.msort_key ?xs) = filter (\<lambda>x. key x = key ?x3) ?xs

goal (1 subgoal):
 1. sort_key key = local.msort_key
[PROOF STEP]
by (intro ext properties_for_sort_key mset_msort_key sorted_msort_key)
    (metis (mono_tags, lifting) filter_cong)


[STATEMENT]
lemma in_range_empty[simp, intro!]: "in_range (h,{})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_range (h, {})
[PROOF STEP]
by (auto simp: in_range.simps)


[STATEMENT]
lemma in_range_dist_union[simp]:
  "in_range (h,as \<union> as') \<longleftrightarrow> in_range (h,as) \<and> in_range (h,as')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_range (h, as \<union> as') = (in_range (h, as) \<and> in_range (h, as'))
[PROOF STEP]
by (auto simp: in_range.simps)


[STATEMENT]
lemma in_range_subset:
  "\<lbrakk>as \<subseteq> as'; in_range (h,as')\<rbrakk> \<Longrightarrow> in_range (h,as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>as \<subseteq> as'; in_range (h, as')\<rbrakk> \<Longrightarrow> in_range (h, as)
[PROOF STEP]
by (auto simp: in_range.simps)


[STATEMENT]
lemma relH_in_rangeI:
  assumes "relH as h h'"
  shows "in_range (h,as)" and "in_range (h',as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_range (h, as) &&& in_range (h', as)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
relH as h h'

goal (1 subgoal):
 1. in_range (h, as) &&& in_range (h', as)
[PROOF STEP]
unfolding relH_def
[PROOF STATE]
proof (prove)
using this:
in_range (h, as) \<and> in_range (h', as) \<and> (\<forall>t. \<forall>a\<in>as. refs h t a = refs h' t a \<and> arrays h t a = arrays h' t a)

goal (1 subgoal):
 1. in_range (h, as) &&& in_range (h', as)
[PROOF STEP]
by auto


[STATEMENT]
lemma relH_refl: "in_range (h,as) \<Longrightarrow> relH as h h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_range (h, as) \<Longrightarrow> relH as h h
[PROOF STEP]
unfolding relH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_range (h, as) \<Longrightarrow> in_range (h, as) \<and> in_range (h, as) \<and> (\<forall>t. \<forall>a\<in>as. refs h t a = refs h t a \<and> arrays h t a = arrays h t a)
[PROOF STEP]
by simp


[STATEMENT]
lemma relH_sym: "relH as h h' \<Longrightarrow> relH as h' h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relH as h h' \<Longrightarrow> relH as h' h
[PROOF STEP]
unfolding relH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_range (h, as) \<and> in_range (h', as) \<and> (\<forall>t. \<forall>a\<in>as. refs h t a = refs h' t a \<and> arrays h t a = arrays h' t a) \<Longrightarrow> in_range (h', as) \<and> in_range (h, as) \<and> (\<forall>t. \<forall>a\<in>as. refs h' t a = refs h t a \<and> arrays h' t a = arrays h t a)
[PROOF STEP]
by auto


[STATEMENT]
lemma relH_trans[trans]: "\<lbrakk>relH as h1 h2; relH as h2 h3\<rbrakk> \<Longrightarrow> relH as h1 h3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>relH as h1 h2; relH as h2 h3\<rbrakk> \<Longrightarrow> relH as h1 h3
[PROOF STEP]
unfolding relH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>in_range (h1, as) \<and> in_range (h2, as) \<and> (\<forall>t. \<forall>a\<in>as. refs h1 t a = refs h2 t a \<and> arrays h1 t a = arrays h2 t a); in_range (h2, as) \<and> in_range (h3, as) \<and> (\<forall>t. \<forall>a\<in>as. refs h2 t a = refs h3 t a \<and> arrays h2 t a = arrays h3 t a)\<rbrakk> \<Longrightarrow> in_range (h1, as) \<and> in_range (h3, as) \<and> (\<forall>t. \<forall>a\<in>as. refs h1 t a = refs h3 t a \<and> arrays h1 t a = arrays h3 t a)
[PROOF STEP]
by auto


[STATEMENT]
lemma relH_dist_union[simp]:
  "relH (as\<union>as') h h' \<longleftrightarrow> relH as h h' \<and> relH as' h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relH (as \<union> as') h h' = (relH as h h' \<and> relH as' h h')
[PROOF STEP]
unfolding relH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (in_range (h, as \<union> as') \<and> in_range (h', as \<union> as') \<and> (\<forall>t. \<forall>a\<in>as \<union> as'. refs h t a = refs h' t a \<and> arrays h t a = arrays h' t a)) = ((in_range (h, as) \<and> in_range (h', as) \<and> (\<forall>t. \<forall>a\<in>as. refs h t a = refs h' t a \<and> arrays h t a = arrays h' t a)) \<and> in_range (h, as') \<and> in_range (h', as') \<and> (\<forall>t. \<forall>a\<in>as'. refs h t a = refs h' t a \<and> arrays h t a = arrays h' t a))
[PROOF STEP]
by auto


[STATEMENT]
lemma relH_subset:
  assumes "relH bs h h'"
  assumes "as \<subseteq> bs"
  shows "relH as h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relH as h h'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
relH bs h h'
as \<subseteq> bs

goal (1 subgoal):
 1. relH as h h'
[PROOF STEP]
unfolding relH_def
[PROOF STATE]
proof (prove)
using this:
in_range (h, bs) \<and> in_range (h', bs) \<and> (\<forall>t. \<forall>a\<in>bs. refs h t a = refs h' t a \<and> arrays h t a = arrays h' t a)
as \<subseteq> bs

goal (1 subgoal):
 1. in_range (h, as) \<and> in_range (h', as) \<and> (\<forall>t. \<forall>a\<in>as. refs h t a = refs h' t a \<and> arrays h t a = arrays h' t a)
[PROOF STEP]
by (auto intro: in_range_subset)


[STATEMENT]
lemma relH_ref:
  assumes "relH as h h'"
  assumes "addr_of_ref r \<in> as"
  shows "Ref_Time.get h r = Ref_Time.get h' r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ref_Time.get h r = Ref_Time.get h' r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
relH as h h'
addr_of_ref r \<in> as

goal (1 subgoal):
 1. Ref_Time.get h r = Ref_Time.get h' r
[PROOF STEP]
unfolding relH_def Ref_Time.get_def
[PROOF STATE]
proof (prove)
using this:
in_range (h, as) \<and> in_range (h', as) \<and> (\<forall>t. \<forall>a\<in>as. refs h t a = refs h' t a \<and> arrays h t a = arrays h' t a)
addr_of_ref r \<in> as

goal (1 subgoal):
 1. ((from_nat \<circ>\<circ>\<circ> refs) h TYPEREP('a) \<circ> addr_of_ref) r = ((from_nat \<circ>\<circ>\<circ> refs) h' TYPEREP('a) \<circ> addr_of_ref) r
[PROOF STEP]
by auto


[STATEMENT]
lemma relH_array:
  assumes "relH as h h'"
  assumes "addr_of_array r \<in> as"
  shows "Array_Time.get h r = Array_Time.get h' r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array_Time.get h r = Array_Time.get h' r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
relH as h h'
addr_of_array r \<in> as

goal (1 subgoal):
 1. Array_Time.get h r = Array_Time.get h' r
[PROOF STEP]
unfolding relH_def Array_Time.get_def
[PROOF STATE]
proof (prove)
using this:
in_range (h, as) \<and> in_range (h', as) \<and> (\<forall>t. \<forall>a\<in>as. refs h t a = refs h' t a \<and> arrays h t a = arrays h' t a)
addr_of_array r \<in> as

goal (1 subgoal):
 1. map from_nat (arrays h TYPEREP('a) (addr_of_array r)) = map from_nat (arrays h' TYPEREP('a) (addr_of_array r))
[PROOF STEP]
by auto


[STATEMENT]
lemma relH_set_ref: "\<lbrakk> addr_of_ref r \<notin> as; in_range (h,as)\<rbrakk>
  \<Longrightarrow> relH as h (Ref_Time.set r x h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>addr_of_ref r \<notin> as; in_range (h, as)\<rbrakk> \<Longrightarrow> relH as h (Ref_Time.set r x h)
[PROOF STEP]
unfolding relH_def Ref_Time.set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>addr_of_ref r \<notin> as; in_range (h, as)\<rbrakk> \<Longrightarrow> in_range (h, as) \<and> in_range (refs_update (\<lambda>h. h(TYPEREP('a) := (h TYPEREP('a))(addr_of_ref r := to_nat x))) h, as) \<and> (\<forall>t. \<forall>a\<in>as. refs h t a = refs (refs_update (\<lambda>h. h(TYPEREP('a) := (h TYPEREP('a))(addr_of_ref r := to_nat x))) h) t a \<and> arrays h t a = arrays (refs_update (\<lambda>h. h(TYPEREP('a) := (h TYPEREP('a))(addr_of_ref r := to_nat x))) h) t a)
[PROOF STEP]
by (auto simp: in_range.simps)


[STATEMENT]
lemma relH_set_array: "\<lbrakk>addr_of_array r \<notin> as; in_range (h,as)\<rbrakk>
  \<Longrightarrow> relH as h (Array_Time.set r x h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>addr_of_array r \<notin> as; in_range (h, as)\<rbrakk> \<Longrightarrow> relH as h (Array_Time.set r x h)
[PROOF STEP]
unfolding relH_def Array_Time.set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>addr_of_array r \<notin> as; in_range (h, as)\<rbrakk> \<Longrightarrow> in_range (h, as) \<and> in_range (arrays_update (\<lambda>h. h(TYPEREP('a) := (h TYPEREP('a))(addr_of_array r := map to_nat x))) h, as) \<and> (\<forall>t. \<forall>a\<in>as. refs h t a = refs (arrays_update (\<lambda>h. h(TYPEREP('a) := (h TYPEREP('a))(addr_of_array r := map to_nat x))) h) t a \<and> arrays h t a = arrays (arrays_update (\<lambda>h. h(TYPEREP('a) := (h TYPEREP('a))(addr_of_array r := map to_nat x))) h) t a)
[PROOF STEP]
by (auto simp: in_range.simps)


[STATEMENT]
lemma properI[intro?]:
  assumes "\<And>as h. P (h,as) \<Longrightarrow> in_range (h,as)"
  assumes "\<And>as h h'.
    \<lbrakk>P (h,as); relH as h h'; in_range (h',as)\<rbrakk> \<Longrightarrow> P (h',as)"
  shows "proper P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper P
[PROOF STEP]
unfolding proper_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>h h' as. (P (h, as) \<longrightarrow> in_range (h, as)) \<and> (P (h, as) \<and> relH as h h' \<and> in_range (h', as) \<longrightarrow> P (h', as))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P (?h, ?as) \<Longrightarrow> in_range (?h, ?as)
\<lbrakk>P (?h, ?as); relH ?as ?h ?h'; in_range (?h', ?as)\<rbrakk> \<Longrightarrow> P (?h', ?as)

goal (1 subgoal):
 1. \<forall>h h' as. (P (h, as) \<longrightarrow> in_range (h, as)) \<and> (P (h, as) \<and> relH as h h' \<and> in_range (h', as) \<longrightarrow> P (h', as))
[PROOF STEP]
by blast


[STATEMENT]
lemma properD1:
  assumes "proper P"
  assumes "P (h,as)"
  shows "in_range (h,as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_range (h, as)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
proper P
P (h, as)

goal (1 subgoal):
 1. in_range (h, as)
[PROOF STEP]
unfolding proper_def
[PROOF STATE]
proof (prove)
using this:
\<forall>h h' as. (P (h, as) \<longrightarrow> in_range (h, as)) \<and> (P (h, as) \<and> relH as h h' \<and> in_range (h', as) \<longrightarrow> P (h', as))
P (h, as)

goal (1 subgoal):
 1. in_range (h, as)
[PROOF STEP]
by blast


[STATEMENT]
lemma properD2:
  assumes "proper P"
  assumes "P (h,as)"
  assumes "relH as h h'"
  assumes "in_range (h',as)"
  shows "P (h',as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (h', as)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
proper P
P (h, as)
relH as h h'
in_range (h', as)

goal (1 subgoal):
 1. P (h', as)
[PROOF STEP]
unfolding proper_def
[PROOF STATE]
proof (prove)
using this:
\<forall>h h' as. (P (h, as) \<longrightarrow> in_range (h, as)) \<and> (P (h, as) \<and> relH as h h' \<and> in_range (h', as) \<longrightarrow> P (h', as))
P (h, as)
relH as h h'
in_range (h', as)

goal (1 subgoal):
 1. P (h', as)
[PROOF STEP]
by blast


[STATEMENT]
lemma proper_iff:
  assumes "proper P"
  assumes "relH as h h'"
  assumes "in_range (h',as)"
  shows "P (h,as) \<longleftrightarrow> P (h',as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (h, as) = P (h', as)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
proper P
relH as h h'
in_range (h', as)

goal (1 subgoal):
 1. P (h, as) = P (h', as)
[PROOF STEP]
by (metis properD2 relH_in_rangeI(1) relH_sym)


[STATEMENT]
lemma Abs_assn_eqI[intro?]:
  "(\<And>h. P h = Rep_assn Pr h) \<Longrightarrow> Abs_assn P = Pr"
  "(\<And>h. P h = Rep_assn Pr h) \<Longrightarrow> Pr = Abs_assn P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>h. P h = Rep_assn Pr h) \<Longrightarrow> Abs_assn P = Pr) &&& ((\<And>h. P h = Rep_assn Pr h) \<Longrightarrow> Pr = Abs_assn P)
[PROOF STEP]
by (metis Rep_assn_inverse predicate1I xt1(5))+


[STATEMENT]
lemma models_in_range: "h\<Turnstile>P \<Longrightarrow> in_range h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<Turnstile> P \<Longrightarrow> in_range h
[PROOF STEP]
apply (cases h)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>h \<Turnstile> P; h = (a, b)\<rbrakk> \<Longrightarrow> in_range h
[PROOF STEP]
by (metis mem_Collect_eq Rep_assn properD1)


[STATEMENT]
lemma mod_h_bot_indep: "(h,{})\<Turnstile>P \<longleftrightarrow> (h',{})\<Turnstile>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((h, {}) \<Turnstile> P) = ((h', {}) \<Turnstile> P)
[PROOF STEP]
by (metis mem_Collect_eq Rep_assn emptyE in_range_empty
    proper_iff relH_def)


[STATEMENT]
lemma mod_h_bot_normalize[simp]:
  "syntax_fo_nomatch undefined h \<Longrightarrow> (h,{})\<Turnstile>P \<longleftrightarrow> h\<^sub>\<bottom> \<Turnstile> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. syntax_fo_nomatch undefined h \<Longrightarrow> ((h, {}) \<Turnstile> P) = (h\<^sub>\<bottom> \<Turnstile> P)
[PROOF STEP]
using mod_h_bot_indep[where h'=undefined]
[PROOF STATE]
proof (prove)
using this:
((?h, {}) \<Turnstile> ?P) = (h\<^sub>\<bottom> \<Turnstile> ?P)

goal (1 subgoal):
 1. syntax_fo_nomatch undefined h \<Longrightarrow> ((h, {}) \<Turnstile> P) = (h\<^sub>\<bottom> \<Turnstile> P)
[PROOF STEP]
by simp


[STATEMENT]
lemma mod_relH: "relH as h h' \<Longrightarrow> (h,as)\<Turnstile>P \<longleftrightarrow> (h',as)\<Turnstile>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relH as h h' \<Longrightarrow> ((h, as) \<Turnstile> P) = ((h', as) \<Turnstile> P)
[PROOF STEP]
by (metis mem_Collect_eq Rep_assn proper_iff relH_in_rangeI(2))


[STATEMENT]
lemma one_assn_proper[intro!,simp]: "proper one_assn_raw"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper one_assn_raw
[PROOF STEP]
by (auto intro!: properI)


[STATEMENT]
lemma times_assn_proper[intro!,simp]:
    "proper P \<Longrightarrow> proper Q \<Longrightarrow> proper (times_assn_raw P Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>proper P; proper Q\<rbrakk> \<Longrightarrow> proper (times_assn_raw P Q)
[PROOF STEP]
apply (rule properI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as h. \<lbrakk>proper P; proper Q; times_assn_raw P Q (h, as)\<rbrakk> \<Longrightarrow> in_range (h, as)
 2. \<And>as h h'. \<lbrakk>proper P; proper Q; times_assn_raw P Q (h, as); relH as h h'; in_range (h', as)\<rbrakk> \<Longrightarrow> times_assn_raw P Q (h', as)
[PROOF STEP]
apply (auto dest: properD1) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as h h'. \<lbrakk>proper P; proper Q; times_assn_raw P Q (h, as); relH as h h'; in_range (h', as)\<rbrakk> \<Longrightarrow> times_assn_raw P Q (h', as)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h' as1 as2. \<lbrakk>proper P; proper Q; as1 \<inter> as2 = {}; P (h, as1); Q (h, as2); relH as1 h h'; relH as2 h h'; in_range (h', as1); in_range (h', as2)\<rbrakk> \<Longrightarrow> \<exists>as1a as2a. as1 \<union> as2 = as1a \<union> as2a \<and> as1a \<inter> as2a = {} \<and> P (h', as1a) \<and> Q (h', as2a)
[PROOF STEP]
apply (drule (3) properD2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h' as1 as2. \<lbrakk>proper Q; as1 \<inter> as2 = {}; P (h, as1); Q (h, as2); relH as1 h h'; relH as2 h h'; in_range (h', as1); in_range (h', as2); P (h', as1)\<rbrakk> \<Longrightarrow> \<exists>as1a as2a. as1 \<union> as2 = as1a \<union> as2a \<and> as1a \<inter> as2a = {} \<and> P (h', as1a) \<and> Q (h', as2a)
[PROOF STEP]
apply (drule (3) properD2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h' as1 as2. \<lbrakk>as1 \<inter> as2 = {}; P (h, as1); Q (h, as2); relH as1 h h'; relH as2 h h'; in_range (h', as1); in_range (h', as2); P (h', as1); Q (h', as2)\<rbrakk> \<Longrightarrow> \<exists>as1a as2a. as1 \<union> as2 = as1a \<union> as2a \<and> as1a \<inter> as2a = {} \<and> P (h', as1a) \<and> Q (h', as2a)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mod_star_conv: "h\<Turnstile>A*B
  \<longleftrightarrow> (\<exists>hr as1 as2. h=(hr,as1\<union>as2) \<and> as1\<inter>as2={} \<and> (hr,as1)\<Turnstile>A \<and> (hr,as2)\<Turnstile>B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> A * B) = (\<exists>hr as1 as2. h = (hr, as1 \<union> as2) \<and> as1 \<inter> as2 = {} \<and> (hr, as1) \<Turnstile> A \<and> (hr, as2) \<Turnstile> B)
[PROOF STEP]
unfolding times_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn A) (Rep_assn B))) = (\<exists>hr as1 as2. h = (hr, as1 \<union> as2) \<and> as1 \<inter> as2 = {} \<and> (hr, as1) \<Turnstile> A \<and> (hr, as2) \<Turnstile> B)
[PROOF STEP]
apply (cases h)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. h = (a, b) \<Longrightarrow> (h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn A) (Rep_assn B))) = (\<exists>hr as1 as2. h = (hr, as1 \<union> as2) \<and> as1 \<inter> as2 = {} \<and> (hr, as1) \<Turnstile> A \<and> (hr, as2) \<Turnstile> B)
[PROOF STEP]
by (auto simp: Abs_assn_inverse)


[STATEMENT]
lemma mod_starD: "h\<Turnstile>A*B \<Longrightarrow> \<exists>h1 h2. h1\<Turnstile>A \<and> h2\<Turnstile>B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<Turnstile> A * B \<Longrightarrow> \<exists>h1 h2. h1 \<Turnstile> A \<and> h2 \<Turnstile> B
[PROOF STEP]
by (auto simp: mod_star_conv)


[STATEMENT]
lemma mod_starE:
  assumes "h \<Turnstile> a*b"
  obtains h\<^sub>1 h\<^sub>2 where "h\<^sub>1 \<Turnstile> a" "h\<^sub>2 \<Turnstile> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h\<^sub>1 h\<^sub>2. \<lbrakk>h\<^sub>1 \<Turnstile> a; h\<^sub>2 \<Turnstile> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> a * b

goal (1 subgoal):
 1. (\<And>h\<^sub>1 h\<^sub>2. \<lbrakk>h\<^sub>1 \<Turnstile> a; h\<^sub>2 \<Turnstile> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: mod_starD)


[STATEMENT]
lemma star_assnI:
  assumes "(h,as)\<Turnstile>P" and "(h,as')\<Turnstile>Q" and "as\<inter>as'={}"
  shows "(h,as\<union>as')\<Turnstile>P*Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h, as \<union> as') \<Turnstile> P * Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(h, as) \<Turnstile> P
(h, as') \<Turnstile> Q
as \<inter> as' = {}

goal (1 subgoal):
 1. (h, as \<union> as') \<Turnstile> P * Q
[PROOF STEP]
unfolding times_assn_def
[PROOF STATE]
proof (prove)
using this:
(h, as) \<Turnstile> P
(h, as') \<Turnstile> Q
as \<inter> as' = {}

goal (1 subgoal):
 1. (h, as \<union> as') \<Turnstile> Abs_assn (times_assn_raw (Rep_assn P) (Rep_assn Q))
[PROOF STEP]
by (auto simp: Abs_assn_inverse)


[STATEMENT]
lemma assn_one_left: "1*P = (P::assn)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emp * P = P
[PROOF STEP]
unfolding one_assn_def times_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (times_assn_raw (Rep_assn (Abs_assn one_assn_raw)) (Rep_assn P)) = P
[PROOF STEP]
apply (rule)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. times_assn_raw (Rep_assn (Abs_assn one_assn_raw)) (Rep_assn P) h = (h \<Turnstile> P)
[PROOF STEP]
apply (auto simp: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma assn_times_comm: "P*Q = Q*(P::assn)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * Q = Q * P
[PROOF STEP]
unfolding times_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (times_assn_raw (Rep_assn P) (Rep_assn Q)) = Abs_assn (times_assn_raw (Rep_assn Q) (Rep_assn P))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. times_assn_raw (Rep_assn Q) (Rep_assn P) h = (h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn P) (Rep_assn Q)))
[PROOF STEP]
apply (fastforce simp add: Abs_assn_inverse Un_ac)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma assn_times_assoc: "(P*Q)*R = P*(Q*(R::assn))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * Q * R = P * (Q * R)
[PROOF STEP]
unfolding times_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (times_assn_raw (Rep_assn (Abs_assn (times_assn_raw (Rep_assn P) (Rep_assn Q)))) (Rep_assn R)) = Abs_assn (times_assn_raw (Rep_assn P) (Rep_assn (Abs_assn (times_assn_raw (Rep_assn Q) (Rep_assn R)))))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. times_assn_raw (Rep_assn P) (Rep_assn (Abs_assn (times_assn_raw (Rep_assn Q) (Rep_assn R)))) h = (h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn (Abs_assn (times_assn_raw (Rep_assn P) (Rep_assn Q)))) (Rep_assn R)))
[PROOF STEP]
apply (auto simp: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as1 as1a as2a. \<lbrakk>as1 \<inter> (as1a \<union> as2a) = {}; (a, as1) \<Turnstile> P; as1a \<inter> as2a = {}; (a, as1a) \<Turnstile> Q; (a, as2a) \<Turnstile> R\<rbrakk> \<Longrightarrow> \<exists>as1b as2. as1 \<union> (as1a \<union> as2a) = as1b \<union> as2 \<and> as1b \<inter> as2 = {} \<and> (\<exists>as1 as2. as1b = as1 \<union> as2 \<and> as1 \<inter> as2 = {} \<and> (a, as1) \<Turnstile> P \<and> (a, as2) \<Turnstile> Q) \<and> (a, as2) \<Turnstile> R
 2. \<And>a as2 as1a as2a. \<lbrakk>(as1a \<union> as2a) \<inter> as2 = {}; (a, as2) \<Turnstile> R; as1a \<inter> as2a = {}; (a, as1a) \<Turnstile> P; (a, as2a) \<Turnstile> Q\<rbrakk> \<Longrightarrow> \<exists>as1 as2b. as1a \<union> as2a \<union> as2 = as1 \<union> as2b \<and> as1 \<inter> as2b = {} \<and> (a, as1) \<Turnstile> P \<and> (\<exists>as1 as2. as2b = as1 \<union> as2 \<and> as1 \<inter> as2 = {} \<and> (a, as1) \<Turnstile> Q \<and> (a, as2) \<Turnstile> R)
[PROOF STEP]
apply (rule_tac x="as1\<union>as1a" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as1 as1a as2a. \<lbrakk>as1 \<inter> (as1a \<union> as2a) = {}; (a, as1) \<Turnstile> P; as1a \<inter> as2a = {}; (a, as1a) \<Turnstile> Q; (a, as2a) \<Turnstile> R\<rbrakk> \<Longrightarrow> \<exists>as2. as1 \<union> (as1a \<union> as2a) = as1 \<union> as1a \<union> as2 \<and> (as1 \<union> as1a) \<inter> as2 = {} \<and> (\<exists>as1b as2. as1 \<union> as1a = as1b \<union> as2 \<and> as1b \<inter> as2 = {} \<and> (a, as1b) \<Turnstile> P \<and> (a, as2) \<Turnstile> Q) \<and> (a, as2) \<Turnstile> R
 2. \<And>a as2 as1a as2a. \<lbrakk>(as1a \<union> as2a) \<inter> as2 = {}; (a, as2) \<Turnstile> R; as1a \<inter> as2a = {}; (a, as1a) \<Turnstile> P; (a, as2a) \<Turnstile> Q\<rbrakk> \<Longrightarrow> \<exists>as1 as2b. as1a \<union> as2a \<union> as2 = as1 \<union> as2b \<and> as1 \<inter> as2b = {} \<and> (a, as1) \<Turnstile> P \<and> (\<exists>as1 as2. as2b = as1 \<union> as2 \<and> as1 \<inter> as2 = {} \<and> (a, as1) \<Turnstile> Q \<and> (a, as2) \<Turnstile> R)
[PROOF STEP]
apply (rule_tac x="as2a" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as1 as1a as2a. \<lbrakk>as1 \<inter> (as1a \<union> as2a) = {}; (a, as1) \<Turnstile> P; as1a \<inter> as2a = {}; (a, as1a) \<Turnstile> Q; (a, as2a) \<Turnstile> R\<rbrakk> \<Longrightarrow> as1 \<union> (as1a \<union> as2a) = as1 \<union> as1a \<union> as2a \<and> (as1 \<union> as1a) \<inter> as2a = {} \<and> (\<exists>as1b as2. as1 \<union> as1a = as1b \<union> as2 \<and> as1b \<inter> as2 = {} \<and> (a, as1b) \<Turnstile> P \<and> (a, as2) \<Turnstile> Q) \<and> (a, as2a) \<Turnstile> R
 2. \<And>a as2 as1a as2a. \<lbrakk>(as1a \<union> as2a) \<inter> as2 = {}; (a, as2) \<Turnstile> R; as1a \<inter> as2a = {}; (a, as1a) \<Turnstile> P; (a, as2a) \<Turnstile> Q\<rbrakk> \<Longrightarrow> \<exists>as1 as2b. as1a \<union> as2a \<union> as2 = as1 \<union> as2b \<and> as1 \<inter> as2b = {} \<and> (a, as1) \<Turnstile> P \<and> (\<exists>as1 as2. as2b = as1 \<union> as2 \<and> as1 \<inter> as2 = {} \<and> (a, as1) \<Turnstile> Q \<and> (a, as2) \<Turnstile> R)
[PROOF STEP]
apply (auto simp add: Un_ac) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as2 as1a as2a. \<lbrakk>(as1a \<union> as2a) \<inter> as2 = {}; (a, as2) \<Turnstile> R; as1a \<inter> as2a = {}; (a, as1a) \<Turnstile> P; (a, as2a) \<Turnstile> Q\<rbrakk> \<Longrightarrow> \<exists>as1 as2b. as1a \<union> as2a \<union> as2 = as1 \<union> as2b \<and> as1 \<inter> as2b = {} \<and> (a, as1) \<Turnstile> P \<and> (\<exists>as1 as2. as2b = as1 \<union> as2 \<and> as1 \<inter> as2 = {} \<and> (a, as1) \<Turnstile> Q \<and> (a, as2) \<Turnstile> R)
[PROOF STEP]
apply (rule_tac x="as1a" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as2 as1a as2a. \<lbrakk>(as1a \<union> as2a) \<inter> as2 = {}; (a, as2) \<Turnstile> R; as1a \<inter> as2a = {}; (a, as1a) \<Turnstile> P; (a, as2a) \<Turnstile> Q\<rbrakk> \<Longrightarrow> \<exists>as2b. as1a \<union> as2a \<union> as2 = as1a \<union> as2b \<and> as1a \<inter> as2b = {} \<and> (a, as1a) \<Turnstile> P \<and> (\<exists>as1 as2. as2b = as1 \<union> as2 \<and> as1 \<inter> as2 = {} \<and> (a, as1) \<Turnstile> Q \<and> (a, as2) \<Turnstile> R)
[PROOF STEP]
apply (rule_tac x="as2a\<union>as2" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as2 as1a as2a. \<lbrakk>(as1a \<union> as2a) \<inter> as2 = {}; (a, as2) \<Turnstile> R; as1a \<inter> as2a = {}; (a, as1a) \<Turnstile> P; (a, as2a) \<Turnstile> Q\<rbrakk> \<Longrightarrow> as1a \<union> as2a \<union> as2 = as1a \<union> (as2a \<union> as2) \<and> as1a \<inter> (as2a \<union> as2) = {} \<and> (a, as1a) \<Turnstile> P \<and> (\<exists>as1 as2b. as2a \<union> as2 = as1 \<union> as2b \<and> as1 \<inter> as2b = {} \<and> (a, as1) \<Turnstile> Q \<and> (a, as2b) \<Turnstile> R)
[PROOF STEP]
apply (fastforce simp add: Un_ac) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wand_proper[simp, intro!]: "proper (wand_raw P Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper (wand_raw P Q)
[PROOF STEP]
apply (rule properI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as h. wand_raw P Q (h, as) \<Longrightarrow> in_range (h, as)
 2. \<And>as h h'. \<lbrakk>wand_raw P Q (h, as); relH as h h'; in_range (h', as)\<rbrakk> \<Longrightarrow> wand_raw P Q (h', as)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as h h'. \<lbrakk>wand_raw P Q (h, as); relH as h h'; in_range (h', as)\<rbrakk> \<Longrightarrow> wand_raw P Q (h', as)
[PROOF STEP]
apply (auto dest: relH_trans)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wand_assnI:
  assumes "in_range (h,as)"
  assumes "\<And>h' as'. \<lbrakk>
    as \<inter> as' = {};
    relH as h h';
    in_range (h',as);
    (h',as')\<Turnstile>Q
  \<rbrakk> \<Longrightarrow> (h',as\<union>as') \<Turnstile> R"
  shows "(h,as) \<Turnstile> Q -* R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h, as) \<Turnstile> Q -* R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
in_range (h, as)
\<lbrakk>as \<inter> ?as' = {}; relH as h ?h'; in_range (?h', as); (?h', ?as') \<Turnstile> Q\<rbrakk> \<Longrightarrow> (?h', as \<union> ?as') \<Turnstile> R

goal (1 subgoal):
 1. (h, as) \<Turnstile> Q -* R
[PROOF STEP]
unfolding wand_assn_def
[PROOF STATE]
proof (prove)
using this:
in_range (h, as)
\<lbrakk>as \<inter> ?as' = {}; relH as h ?h'; in_range (?h', as); (?h', ?as') \<Turnstile> Q\<rbrakk> \<Longrightarrow> (?h', as \<union> ?as') \<Turnstile> R

goal (1 subgoal):
 1. (h, as) \<Turnstile> Abs_assn (wand_raw (Rep_assn Q) (Rep_assn R))
[PROOF STEP]
apply (auto simp: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bool_assn_proper[simp, intro!]:
    "proper in_range"
    "proper (\<lambda>_. False)"
    "proper P \<Longrightarrow> proper Q \<Longrightarrow> proper (\<lambda>h. P h \<or> Q h)"
    "proper P \<Longrightarrow> proper Q \<Longrightarrow> proper (\<lambda>h. P h \<and> Q h)"
    "proper P \<Longrightarrow> proper (\<lambda>h. in_range h \<and> \<not>P h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (proper in_range &&& proper (\<lambda>_. False)) &&& (\<lbrakk>proper P; proper Q\<rbrakk> \<Longrightarrow> proper (\<lambda>h. P h \<or> Q h)) &&& (\<lbrakk>proper P; proper Q\<rbrakk> \<Longrightarrow> proper (\<lambda>h. P h \<and> Q h)) &&& (proper P \<Longrightarrow> proper (\<lambda>h. in_range h \<and> \<not> P h))
[PROOF STEP]
apply (auto
      intro!: properI
      intro: relH_in_rangeI
      dest: properD1
      simp: proper_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma star_false_left[simp]: "false * P = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. false * P = false
[PROOF STEP]
unfolding times_assn_def bot_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (times_assn_raw (Rep_assn (Abs_assn (\<lambda>_. False))) (Rep_assn P)) = Abs_assn (\<lambda>_. False)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. False = (h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn (Abs_assn (\<lambda>_. False))) (Rep_assn P)))
[PROOF STEP]
apply (auto simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma star_false_right[simp]: "P * false = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * false = false
[PROOF STEP]
using star_false_left
[PROOF STATE]
proof (prove)
using this:
false * ?P = false

goal (1 subgoal):
 1. P * false = false
[PROOF STEP]
by (simp add: assn_times_comm)


[STATEMENT]
lemma assn_basic_inequalities[simp, intro!]:
  "true \<noteq> emp" "emp \<noteq> true"
  "false \<noteq> emp" "emp \<noteq> false"
  "true \<noteq> false" "false \<noteq> true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (true \<noteq> emp &&& emp \<noteq> true &&& false \<noteq> emp) &&& emp \<noteq> false &&& true \<noteq> false &&& false \<noteq> true
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. true \<noteq> emp
[PROOF STEP]
unfolding one_assn_def top_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn in_range \<noteq> Abs_assn one_assn_raw
[PROOF STEP]
proof (subst Abs_assn_inject; simp?)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. in_range \<noteq> one_assn_raw
[PROOF STEP]
have "in_range (\<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 1\<rparr>,{0})" (is "in_range ?h")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_range (\<lparr>arrays = \<lambda>_ _. [], refs = \<lambda>_ _. 0, lim = 1\<rparr>, {0})
[PROOF STEP]
by (auto simp: in_range.simps)
[PROOF STATE]
proof (state)
this:
in_range (\<lparr>arrays = \<lambda>_ _. [], refs = \<lambda>_ _. 0, lim = 1\<rparr>, {0})

goal (1 subgoal):
 1. in_range \<noteq> one_assn_raw
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
in_range (\<lparr>arrays = \<lambda>_ _. [], refs = \<lambda>_ _. 0, lim = 1\<rparr>, {0})

goal (1 subgoal):
 1. in_range \<noteq> one_assn_raw
[PROOF STEP]
have "\<not>one_assn_raw ?h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> one_assn_raw (\<lparr>arrays = \<lambda>_ _. [], refs = \<lambda>_ _. 0, lim = 1\<rparr>, {0})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> one_assn_raw (\<lparr>arrays = \<lambda>_ _. [], refs = \<lambda>_ _. 0, lim = 1\<rparr>, {0})

goal (1 subgoal):
 1. in_range \<noteq> one_assn_raw
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
in_range (\<lparr>arrays = \<lambda>_ _. [], refs = \<lambda>_ _. 0, lim = 1\<rparr>, {0})
\<not> one_assn_raw (\<lparr>arrays = \<lambda>_ _. [], refs = \<lambda>_ _. 0, lim = 1\<rparr>, {0})
[PROOF STEP]
show "in_range \<noteq> one_assn_raw"
[PROOF STATE]
proof (prove)
using this:
in_range (\<lparr>arrays = \<lambda>_ _. [], refs = \<lambda>_ _. 0, lim = 1\<rparr>, {0})
\<not> one_assn_raw (\<lparr>arrays = \<lambda>_ _. [], refs = \<lambda>_ _. 0, lim = 1\<rparr>, {0})

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. emp \<noteq> true
 2. false \<noteq> emp
 3. emp \<noteq> false
 4. true \<noteq> false
 5. false \<noteq> true
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emp \<noteq> true
[PROOF STEP]
by (simp add: \<open>true \<noteq> emp\<close>)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. false \<noteq> emp
 2. emp \<noteq> false
 3. true \<noteq> false
 4. false \<noteq> true
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. false \<noteq> emp
[PROOF STEP]
using star_false_left \<open>true \<noteq> emp\<close>
[PROOF STATE]
proof (prove)
using this:
false * ?P = false
true \<noteq> emp

goal (1 subgoal):
 1. false \<noteq> emp
[PROOF STEP]
by force
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. emp \<noteq> false
 2. true \<noteq> false
 3. false \<noteq> true
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emp \<noteq> false
[PROOF STEP]
by (simp add: \<open>false \<noteq> emp\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. true \<noteq> false
 2. false \<noteq> true
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. true \<noteq> false
[PROOF STEP]
by (metis inf_bot_right inf_top.right_neutral \<open>true \<noteq> emp\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. false \<noteq> true
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. false \<noteq> true
[PROOF STEP]
using \<open>true \<noteq> false\<close>
[PROOF STATE]
proof (prove)
using this:
true \<noteq> false

goal (1 subgoal):
 1. false \<noteq> true
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ex_assn_proper[simp, intro!]:
  "(\<And>x. proper (P x)) \<Longrightarrow> proper (\<lambda>h. \<exists>x. P x h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. proper (P x)) \<Longrightarrow> proper (\<lambda>h. \<exists>x. P x h)
[PROOF STEP]
by (auto intro!: properI dest: properD1 simp: proper_iff)


[STATEMENT]
lemma ex_assn_const[simp]: "(\<exists>\<^sub>Ax. c) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>\<^sub>Ax. c) = c
[PROOF STEP]
unfolding ex_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> c) = c
[PROOF STEP]
by auto


[STATEMENT]
lemma ex_one_point_gen:
  "\<lbrakk>\<And>h x. h\<Turnstile>P x \<Longrightarrow> x=v\<rbrakk> \<Longrightarrow> (\<exists>\<^sub>Ax. P x) = (P v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h x. h \<Turnstile> P x \<Longrightarrow> x = v) \<Longrightarrow> (\<exists>\<^sub>Ax. P x) = P v
[PROOF STEP]
unfolding ex_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h x. h \<Turnstile> P x \<Longrightarrow> x = v) \<Longrightarrow> Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> P x) = P v
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. (\<And>h x. h \<Turnstile> P x \<Longrightarrow> x = v) \<Longrightarrow> (\<exists>x. h \<Turnstile> P x) = (h \<Turnstile> P v)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ex_distrib_star: "(\<exists>\<^sub>Ax. P x * Q) = (\<exists>\<^sub>Ax. P x) * Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>\<^sub>Ax. P x * Q) = (\<exists>\<^sub>Ax. P x) * Q
[PROOF STEP]
unfolding ex_assn_def times_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn (P x)) (Rep_assn Q))) = Abs_assn (times_assn_raw (Rep_assn (Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> P x))) (Rep_assn Q))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. times_assn_raw (Rep_assn (Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> P x))) (Rep_assn Q) h = (h \<Turnstile> Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn (P x)) (Rep_assn Q))))
[PROOF STEP]
apply (simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. times_assn_raw (\<lambda>h. \<exists>x. h \<Turnstile> P x) (Rep_assn Q) h = (\<exists>x. times_assn_raw (Rep_assn (P x)) (Rep_assn Q) h)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ex_distrib_and: "(\<exists>\<^sub>Ax. P x \<and>\<^sub>A Q) = (\<exists>\<^sub>Ax. P x) \<and>\<^sub>A Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>\<^sub>Ax. P x \<and>\<^sub>A Q) = (\<exists>\<^sub>Ax. P x) \<and>\<^sub>A Q
[PROOF STEP]
unfolding ex_assn_def inf_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> Abs_assn (\<lambda>h. h \<Turnstile> P x \<and> h \<Turnstile> Q)) = Abs_assn (\<lambda>h. h \<Turnstile> Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> P x) \<and> h \<Turnstile> Q)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. (h \<Turnstile> Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> P x) \<and> h \<Turnstile> Q) = (h \<Turnstile> Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> Abs_assn (\<lambda>h. h \<Turnstile> P x \<and> h \<Turnstile> Q)))
[PROOF STEP]
apply (simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ex_distrib_or: "(\<exists>\<^sub>Ax. P x \<or>\<^sub>A Q) = (\<exists>\<^sub>Ax. P x) \<or>\<^sub>A Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>\<^sub>Ax. P x \<or>\<^sub>A Q) = (\<exists>\<^sub>Ax. P x) \<or>\<^sub>A Q
[PROOF STEP]
unfolding ex_assn_def sup_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> Abs_assn (\<lambda>h. h \<Turnstile> P x \<or> h \<Turnstile> Q)) = Abs_assn (\<lambda>h. h \<Turnstile> Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> P x) \<or> h \<Turnstile> Q)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. (h \<Turnstile> Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> P x) \<or> h \<Turnstile> Q) = (h \<Turnstile> Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> Abs_assn (\<lambda>h. h \<Turnstile> P x \<or> h \<Turnstile> Q)))
[PROOF STEP]
apply (auto simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ex_join_or: "(\<exists>\<^sub>Ax. P x \<or>\<^sub>A (\<exists>\<^sub>Ax. Q x)) = (\<exists>\<^sub>Ax. P x \<or>\<^sub>A Q x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>\<^sub>Ax. P x \<or>\<^sub>A (\<exists>\<^sub>Ax. Q x)) = (\<exists>\<^sub>Ax. P x \<or>\<^sub>A Q x)
[PROOF STEP]
unfolding ex_assn_def sup_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> Abs_assn (\<lambda>h. h \<Turnstile> P x \<or> h \<Turnstile> Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> Q x))) = Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> Abs_assn (\<lambda>h. h \<Turnstile> P x \<or> h \<Turnstile> Q x))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. (\<exists>x. h \<Turnstile> Abs_assn (\<lambda>h. h \<Turnstile> P x \<or> h \<Turnstile> Q x)) = (h \<Turnstile> Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> Abs_assn (\<lambda>h. h \<Turnstile> P x \<or> h \<Turnstile> Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> Q x))))
[PROOF STEP]
apply (auto simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pure_assn_proper[simp, intro!]: "proper (pure_assn_raw b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper (pure_assn_raw b)
[PROOF STEP]
by (auto intro!: properI intro: relH_in_rangeI)


[STATEMENT]
lemma pure_true[simp]: "\<up>True = emp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up> True = emp
[PROOF STEP]
unfolding pure_assn_def one_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (pure_assn_raw True) = Abs_assn one_assn_raw
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. one_assn_raw h = (h \<Turnstile> Abs_assn (pure_assn_raw True))
[PROOF STEP]
apply (simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. one_assn_raw h = pure_assn_raw True h
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pure_false[simp]: "\<up>False = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up> False = false
[PROOF STEP]
unfolding pure_assn_def bot_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (pure_assn_raw False) = Abs_assn (\<lambda>_. False)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. False = (h \<Turnstile> Abs_assn (pure_assn_raw False))
[PROOF STEP]
apply (auto simp: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pure_assn_eq_false_iff[simp]: "\<up>P = false \<longleftrightarrow> \<not>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<up> P = false) = (\<not> P)
[PROOF STEP]
by auto


[STATEMENT]
lemma pure_assn_eq_emp_iff[simp]: "\<up>P = emp \<longleftrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<up> P = emp) = P
[PROOF STEP]
by (cases P) auto


[STATEMENT]
lemma merge_pure_star[simp]:
  "\<up>a * \<up>b = \<up>(a\<and>b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up> a * \<up> b = \<up> (a \<and> b)
[PROOF STEP]
unfolding times_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (times_assn_raw (Rep_assn (\<up> a)) (Rep_assn (\<up> b))) = \<up> (a \<and> b)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. times_assn_raw (Rep_assn (\<up> a)) (Rep_assn (\<up> b)) h = (h \<Turnstile> \<up> (a \<and> b))
[PROOF STEP]
unfolding pure_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. times_assn_raw (Rep_assn (Abs_assn (pure_assn_raw a))) (Rep_assn (Abs_assn (pure_assn_raw b))) h = (h \<Turnstile> Abs_assn (pure_assn_raw (a \<and> b)))
[PROOF STEP]
apply (simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. times_assn_raw (pure_assn_raw a) (pure_assn_raw b) h = pure_assn_raw (a \<and> b) h
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma merge_true_star[simp]: "true*true = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. true * true = true
[PROOF STEP]
unfolding times_assn_def top_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (times_assn_raw (Rep_assn (Abs_assn in_range)) (Rep_assn (Abs_assn in_range))) = Abs_assn in_range
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. in_range h = (h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn (Abs_assn in_range)) (Rep_assn (Abs_assn in_range))))
[PROOF STEP]
apply (simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. in_range h = times_assn_raw in_range in_range h
[PROOF STEP]
apply (fastforce simp: in_range.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma merge_pure_and[simp]:
  "\<up>a \<and>\<^sub>A \<up>b = \<up>(a\<and>b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up> a \<and>\<^sub>A \<up> b = \<up> (a \<and> b)
[PROOF STEP]
unfolding inf_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (\<lambda>h. h \<Turnstile> \<up> a \<and> h \<Turnstile> \<up> b) = \<up> (a \<and> b)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. (h \<Turnstile> \<up> a \<and> h \<Turnstile> \<up> b) = (h \<Turnstile> \<up> (a \<and> b))
[PROOF STEP]
unfolding pure_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. (h \<Turnstile> Abs_assn (pure_assn_raw a) \<and> h \<Turnstile> Abs_assn (pure_assn_raw b)) = (h \<Turnstile> Abs_assn (pure_assn_raw (a \<and> b)))
[PROOF STEP]
apply (simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. (pure_assn_raw a h \<and> pure_assn_raw b h) = pure_assn_raw (a \<and> b) h
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma merge_pure_or[simp]:
  "\<up>a \<or>\<^sub>A \<up>b = \<up>(a\<or>b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up> a \<or>\<^sub>A \<up> b = \<up> (a \<or> b)
[PROOF STEP]
unfolding sup_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (\<lambda>h. h \<Turnstile> \<up> a \<or> h \<Turnstile> \<up> b) = \<up> (a \<or> b)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. (h \<Turnstile> \<up> a \<or> h \<Turnstile> \<up> b) = (h \<Turnstile> \<up> (a \<or> b))
[PROOF STEP]
unfolding pure_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. (h \<Turnstile> Abs_assn (pure_assn_raw a) \<or> h \<Turnstile> Abs_assn (pure_assn_raw b)) = (h \<Turnstile> Abs_assn (pure_assn_raw (a \<or> b)))
[PROOF STEP]
apply (simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. (pure_assn_raw a h \<or> pure_assn_raw b h) = pure_assn_raw (a \<or> b) h
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pure_assn_eq_conv[simp]: "\<up>P = \<up>Q \<longleftrightarrow> P=Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<up> P = \<up> Q) = (P = Q)
[PROOF STEP]
by auto


[STATEMENT]
lemma is_pure_assnE: assumes "is_pure_assn a" obtains P where "a=\<up>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P. a = \<up> P \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_pure_assn a

goal (1 subgoal):
 1. (\<And>P. a = \<up> P \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: is_pure_assn_def)


[STATEMENT]
lemma is_pure_assn_pure[simp, intro!]: "is_pure_assn (\<up>P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_pure_assn (\<up> P)
[PROOF STEP]
by (auto simp add: is_pure_assn_def)


[STATEMENT]
lemma is_pure_assn_basic_simps[simp]:
  "is_pure_assn false"
  "is_pure_assn emp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_pure_assn false &&& is_pure_assn emp
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_pure_assn false
 2. is_pure_assn emp
[PROOF STEP]
have "is_pure_assn (\<up>False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_pure_assn (\<up> False)
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
is_pure_assn (\<up> False)

goal (2 subgoals):
 1. is_pure_assn false
 2. is_pure_assn emp
[PROOF STEP]
thus "is_pure_assn false"
[PROOF STATE]
proof (prove)
using this:
is_pure_assn (\<up> False)

goal (1 subgoal):
 1. is_pure_assn false
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_pure_assn false

goal (1 subgoal):
 1. is_pure_assn emp
[PROOF STEP]
have "is_pure_assn (\<up>True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_pure_assn (\<up> True)
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
is_pure_assn (\<up> True)

goal (1 subgoal):
 1. is_pure_assn emp
[PROOF STEP]
thus "is_pure_assn emp"
[PROOF STATE]
proof (prove)
using this:
is_pure_assn (\<up> True)

goal (1 subgoal):
 1. is_pure_assn emp
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_pure_assn emp

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_pure_assn_starI[simp,intro!]:
  "\<lbrakk>is_pure_assn a; is_pure_assn b\<rbrakk> \<Longrightarrow> is_pure_assn (a*b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_pure_assn a; is_pure_assn b\<rbrakk> \<Longrightarrow> is_pure_assn (a * b)
[PROOF STEP]
by (auto elim!: is_pure_assnE)


[STATEMENT]
lemma sngr_assn_proper[simp, intro!]: "proper (sngr_assn_raw r x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper (sngr_assn_raw r x)
[PROOF STEP]
apply (auto intro!: properI simp: relH_ref)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>h. \<lbrakk>addr_of_ref r < lim h; x = Ref_Time.get h r\<rbrakk> \<Longrightarrow> in_range (h, {addr_of_ref r})
 2. \<And>h h'. \<lbrakk>relH {addr_of_ref r} h h'; in_range (h', {addr_of_ref r}); addr_of_ref r < lim h; x = Ref_Time.get h' r\<rbrakk> \<Longrightarrow> addr_of_ref r < lim h'
[PROOF STEP]
apply (simp add: in_range.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>relH {addr_of_ref r} h h'; in_range (h', {addr_of_ref r}); addr_of_ref r < lim h; x = Ref_Time.get h' r\<rbrakk> \<Longrightarrow> addr_of_ref r < lim h'
[PROOF STEP]
apply (auto simp add: in_range.simps dest: relH_in_rangeI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma snga_assn_proper[simp, intro!]: "proper (snga_assn_raw r x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper (snga_assn_raw r x)
[PROOF STEP]
apply (auto intro!: properI simp: relH_array)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>h. \<lbrakk>addr_of_array r < lim h; x = Array_Time.get h r\<rbrakk> \<Longrightarrow> in_range (h, {addr_of_array r})
 2. \<And>h h'. \<lbrakk>relH {addr_of_array r} h h'; in_range (h', {addr_of_array r}); addr_of_array r < lim h; x = Array_Time.get h' r\<rbrakk> \<Longrightarrow> addr_of_array r < lim h'
[PROOF STEP]
apply (simp add: in_range.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>relH {addr_of_array r} h h'; in_range (h', {addr_of_array r}); addr_of_array r < lim h; x = Array_Time.get h' r\<rbrakk> \<Longrightarrow> addr_of_array r < lim h'
[PROOF STEP]
apply (auto simp add: in_range.simps dest: relH_in_rangeI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sngr_same_false[simp]:
  "p \<mapsto>\<^sub>r x * p \<mapsto>\<^sub>r y = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<mapsto>\<^sub>r x * p \<mapsto>\<^sub>r y = false
[PROOF STEP]
unfolding times_assn_def bot_assn_def sngr_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (times_assn_raw (Rep_assn (Abs_assn (sngr_assn_raw p x))) (Rep_assn (Abs_assn (sngr_assn_raw p y)))) = Abs_assn (\<lambda>_. False)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. False = (h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn (Abs_assn (sngr_assn_raw p x))) (Rep_assn (Abs_assn (sngr_assn_raw p y)))))
[PROOF STEP]
apply (auto simp: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma snga_same_false[simp]:
  "p \<mapsto>\<^sub>a x * p \<mapsto>\<^sub>a y = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<mapsto>\<^sub>a x * p \<mapsto>\<^sub>a y = false
[PROOF STEP]
unfolding times_assn_def bot_assn_def snga_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (times_assn_raw (Rep_assn (Abs_assn (snga_assn_raw p x))) (Rep_assn (Abs_assn (snga_assn_raw p y)))) = Abs_assn (\<lambda>_. False)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. False = (h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn (Abs_assn (snga_assn_raw p x))) (Rep_assn (Abs_assn (snga_assn_raw p y)))))
[PROOF STEP]
apply (auto simp: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mod_true[simp]: "h\<Turnstile>true \<longleftrightarrow> in_range h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> true) = in_range h
[PROOF STEP]
unfolding top_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> Abs_assn in_range) = in_range h
[PROOF STEP]
by (simp add: Abs_assn_inverse)


[STATEMENT]
lemma mod_false[simp]: "\<not> h\<Turnstile>false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> h \<Turnstile> false
[PROOF STEP]
unfolding bot_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> h \<Turnstile> Abs_assn (\<lambda>_. False)
[PROOF STEP]
by (simp add: Abs_assn_inverse)


[STATEMENT]
lemma mod_emp: "h\<Turnstile>emp \<longleftrightarrow> snd h = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> emp) = (snd h = {})
[PROOF STEP]
unfolding one_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> Abs_assn one_assn_raw) = (snd h = {})
[PROOF STEP]
by (cases h) (simp add: Abs_assn_inverse)


[STATEMENT]
lemma mod_emp_simp[simp]: "(h,{})\<Turnstile>emp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h, {}) \<Turnstile> emp
[PROOF STEP]
by (simp add: mod_emp)


[STATEMENT]
lemma mod_pure[simp]: "h\<Turnstile>\<up>b \<longleftrightarrow> snd h = {} \<and> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> \<up> b) = (snd h = {} \<and> b)
[PROOF STEP]
unfolding pure_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> Abs_assn (pure_assn_raw b)) = (snd h = {} \<and> b)
[PROOF STEP]
apply (cases h)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a ba. h = (a, ba) \<Longrightarrow> (h \<Turnstile> Abs_assn (pure_assn_raw b)) = (snd h = {} \<and> b)
[PROOF STEP]
apply (auto simp add: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mod_ex_dist[simp]: "h\<Turnstile>(\<exists>\<^sub>Ax. P x) \<longleftrightarrow> (\<exists>x. h\<Turnstile>P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> (\<exists>\<^sub>Ax. P x)) = (\<exists>x. h \<Turnstile> P x)
[PROOF STEP]
unfolding ex_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> Abs_assn (\<lambda>h. \<exists>x. h \<Turnstile> P x)) = (\<exists>x. h \<Turnstile> P x)
[PROOF STEP]
by (auto simp: Abs_assn_inverse)


[STATEMENT]
lemma mod_exI: "\<exists>x. h\<Turnstile>P x \<Longrightarrow> h\<Turnstile>(\<exists>\<^sub>Ax. P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. h \<Turnstile> P x \<Longrightarrow> h \<Turnstile> (\<exists>\<^sub>Ax. P x)
[PROOF STEP]
by (auto simp: mod_ex_dist)


[STATEMENT]
lemma mod_exE: assumes "h\<Turnstile>(\<exists>\<^sub>Ax. P x)" obtains x where "h\<Turnstile>P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. h \<Turnstile> P x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> (\<exists>\<^sub>Ax. P x)

goal (1 subgoal):
 1. (\<And>x. h \<Turnstile> P x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: mod_ex_dist)


[STATEMENT]
lemma mod_and_dist: "h\<Turnstile>P\<and>\<^sub>AQ \<longleftrightarrow> h\<Turnstile>P \<and> h\<Turnstile>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> P \<and>\<^sub>A Q) = (h \<Turnstile> P \<and> h \<Turnstile> Q)
[PROOF STEP]
unfolding inf_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h \<Turnstile> Abs_assn (\<lambda>h. h \<Turnstile> P \<and> h \<Turnstile> Q)) = (h \<Turnstile> P \<and> h \<Turnstile> Q)
[PROOF STEP]
by (simp add: Abs_assn_inverse)