[STATEMENT]
lemma quasi_isometry_betweenD:
  assumes "lambda C-quasi_isometry_between X Y f"
  shows "lambda C-quasi_isometry_on X f"
        "f`X \<subseteq> Y"
        "\<And>y. y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) y \<le> C"
        "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<le> lambda * dist x y + C"
        "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<ge> (1/lambda) * dist x y - C"
        "lambda \<ge> 1" "C \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lambda C -quasi_isometry_on X f &&& f ` X \<subseteq> Y &&& (\<And>y. y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) y \<le> C)) &&& ((\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (f x) (f y) \<le> lambda * dist x y + C) &&& (\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist x y - C \<le> dist (f x) (f y))) &&& 1 \<le> lambda &&& 0 \<le> C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lambda C -quasi_isometry_between X Y f

goal (1 subgoal):
 1. (lambda C -quasi_isometry_on X f &&& f ` X \<subseteq> Y &&& (\<And>y. y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) y \<le> C)) &&& ((\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (f x) (f y) \<le> lambda * dist x y + C) &&& (\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist x y - C \<le> dist (f x) (f y))) &&& 1 \<le> lambda &&& 0 \<le> C
[PROOF STEP]
unfolding quasi_isometry_between_def quasi_isometry_on_def
[PROOF STATE]
proof (prove)
using this:
(1 \<le> lambda \<and> 0 \<le> C \<and> (\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) \<le> lambda * dist x y + C \<and> 1 / lambda * dist x y - C \<le> dist (f x) (f y))) \<and> f ` X \<subseteq> Y \<and> (\<forall>y\<in>Y. \<exists>x\<in>X. dist (f x) y \<le> C)

goal (1 subgoal):
 1. (1 \<le> lambda \<and> 0 \<le> C \<and> (\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) \<le> lambda * dist x y + C \<and> 1 / lambda * dist x y - C \<le> dist (f x) (f y)) &&& f ` X \<subseteq> Y &&& (\<And>y. y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) y \<le> C)) &&& ((\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (f x) (f y) \<le> lambda * dist x y + C) &&& (\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist x y - C \<le> dist (f x) (f y))) &&& 1 \<le> lambda &&& 0 \<le> C
[PROOF STEP]
by auto


[STATEMENT]
lemma quasi_isometry_betweenI:
  assumes "lambda C-quasi_isometry_on X f"
          "f`X \<subseteq> Y"
          "\<And>y. y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) y \<le> C"
  shows "lambda C-quasi_isometry_between X Y f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda C -quasi_isometry_between X Y f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lambda C -quasi_isometry_on X f
f ` X \<subseteq> Y
?y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) ?y \<le> C

goal (1 subgoal):
 1. lambda C -quasi_isometry_between X Y f
[PROOF STEP]
unfolding quasi_isometry_between_def
[PROOF STATE]
proof (prove)
using this:
lambda C -quasi_isometry_on X f
f ` X \<subseteq> Y
?y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) ?y \<le> C

goal (1 subgoal):
 1. lambda C -quasi_isometry_on X f \<and> f ` X \<subseteq> Y \<and> (\<forall>y\<in>Y. \<exists>x\<in>X. dist (f x) y \<le> C)
[PROOF STEP]
by auto


[STATEMENT]
lemma quasi_isometry_on_between:
  assumes "lambda C-quasi_isometry_on X f"
  shows "lambda C-quasi_isometry_between X (f`X) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda C -quasi_isometry_between X (f ` X) f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lambda C -quasi_isometry_on X f

goal (1 subgoal):
 1. lambda C -quasi_isometry_between X (f ` X) f
[PROOF STEP]
unfolding quasi_isometry_between_def quasi_isometry_on_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> lambda \<and> 0 \<le> C \<and> (\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) \<le> lambda * dist x y + C \<and> 1 / lambda * dist x y - C \<le> dist (f x) (f y))

goal (1 subgoal):
 1. (1 \<le> lambda \<and> 0 \<le> C \<and> (\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) \<le> lambda * dist x y + C \<and> 1 / lambda * dist x y - C \<le> dist (f x) (f y))) \<and> f ` X \<subseteq> f ` X \<and> (\<forall>y\<in>f ` X. \<exists>x\<in>X. dist (f x) y \<le> C)
[PROOF STEP]
by force


[STATEMENT]
lemma quasi_isometry_between_change_params:
  assumes "lambda C-quasi_isometry_between X Y f" "mu \<ge> lambda" "D \<ge> C"
  shows "mu D-quasi_isometry_between X Y f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mu D -quasi_isometry_between X Y f
[PROOF STEP]
proof (rule quasi_isometry_betweenI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. mu D -quasi_isometry_on X f
 2. f ` X \<subseteq> Y
 3. \<And>y. y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) y \<le> D
[PROOF STEP]
show "mu D-quasi_isometry_on X f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mu D -quasi_isometry_on X f
[PROOF STEP]
by (rule quasi_isometry_on_change_params[OF quasi_isometry_betweenD(1)[OF assms(1)] assms(2) assms(3)])
[PROOF STATE]
proof (state)
this:
mu D -quasi_isometry_on X f

goal (2 subgoals):
 1. f ` X \<subseteq> Y
 2. \<And>y. y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) y \<le> D
[PROOF STEP]
show "f`X \<subseteq> Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` X \<subseteq> Y
[PROOF STEP]
using quasi_isometry_betweenD[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
lambda C -quasi_isometry_on X f
f ` X \<subseteq> Y
?y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) ?y \<le> C
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist ?x ?y - C \<le> dist (f ?x) (f ?y)
1 \<le> lambda
0 \<le> C

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

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) y \<le> D
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) y \<le> D
[PROOF STEP]
assume "y \<in> Y"
[PROOF STATE]
proof (state)
this:
y \<in> Y

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) y \<le> D
[PROOF STEP]
show "\<exists>x\<in>X. dist (f x) y \<le> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>X. dist (f x) y \<le> D
[PROOF STEP]
using quasi_isometry_betweenD(3)[OF assms(1) \<open>y \<in> Y\<close>] \<open>D \<ge> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>X. dist (f x) y \<le> C
C \<le> D

goal (1 subgoal):
 1. \<exists>x\<in>X. dist (f x) y \<le> D
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>X. dist (f x) y \<le> D

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quasi_isometry_subset:
  assumes "X \<subseteq> Y" "\<And>y. y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist x y \<le> C" "C \<ge> 0"
  shows "1 C-quasi_isometry_between X Y (\<lambda>x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 C -quasi_isometry_between X Y (\<lambda>x. x)
[PROOF STEP]
unfolding quasi_isometry_between_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 C -quasi_isometry_on X (\<lambda>x. x) \<and> (\<lambda>x. x) ` X \<subseteq> Y \<and> (\<forall>y\<in>Y. \<exists>x\<in>X. dist x y \<le> C)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> Y
?y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist x ?y \<le> C
0 \<le> C

goal (1 subgoal):
 1. 1 C -quasi_isometry_on X (\<lambda>x. x) \<and> (\<lambda>x. x) ` X \<subseteq> Y \<and> (\<forall>y\<in>Y. \<exists>x\<in>X. dist x y \<le> C)
[PROOF STEP]
by auto


[STATEMENT]
lemma isometry_quasi_isometry_between:
  assumes "isometry f"
  shows "1 0-quasi_isometry_between UNIV UNIV f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 0 -quasi_isometry_between UNIV UNIV f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isometry f

goal (1 subgoal):
 1. 1 0 -quasi_isometry_between UNIV UNIV f
[PROOF STEP]
unfolding quasi_isometry_between_def quasi_isometry_on_def isometry_def isometry_on_def surj_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>UNIV. \<forall>y\<in>UNIV. dist (f x) (f y) = dist x y) \<and> (\<forall>y. \<exists>x. y = f x)

goal (1 subgoal):
 1. (1 \<le> 1 \<and> 0 \<le> 0 \<and> (\<forall>x\<in>UNIV. \<forall>y\<in>UNIV. dist (f x) (f y) \<le> 1 * dist x y + 0 \<and> 1 / 1 * dist x y - 0 \<le> dist (f x) (f y))) \<and> range f \<subseteq> UNIV \<and> (\<forall>y\<in>UNIV. \<exists>x\<in>UNIV. dist (f x) y \<le> 0)
[PROOF STEP]
by (auto) metis


[STATEMENT]
theorem quasi_isometric_equiv_rel:
  "quasi_isometric X X"
  "quasi_isometric X Y \<Longrightarrow> quasi_isometric Y Z \<Longrightarrow> quasi_isometric X Z"
  "quasi_isometric X Y \<Longrightarrow> quasi_isometric Y X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quasi_isometric X X &&& (\<lbrakk>quasi_isometric X Y; quasi_isometric Y Z\<rbrakk> \<Longrightarrow> quasi_isometric X Z) &&& (quasi_isometric X Y \<Longrightarrow> quasi_isometric Y X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. quasi_isometric X X
 2. \<lbrakk>quasi_isometric X Y; quasi_isometric Y Z\<rbrakk> \<Longrightarrow> quasi_isometric X Z
 3. quasi_isometric X Y \<Longrightarrow> quasi_isometric Y X
[PROOF STEP]
show "quasi_isometric X X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quasi_isometric X X
[PROOF STEP]
unfolding quasi_isometric_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>lambda C. Ex (lambda C -quasi_isometry_between X X)
[PROOF STEP]
using quasi_isometry_subset[of X X 0]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>X \<subseteq> X; \<And>y. y \<in> X \<Longrightarrow> \<exists>x\<in>X. dist x y \<le> 0; 0 \<le> 0\<rbrakk> \<Longrightarrow> 1 0 -quasi_isometry_between X X (\<lambda>x. x)

goal (1 subgoal):
 1. \<exists>lambda C. Ex (lambda C -quasi_isometry_between X X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
quasi_isometric X X

goal (2 subgoals):
 1. \<lbrakk>quasi_isometric X Y; quasi_isometric Y Z\<rbrakk> \<Longrightarrow> quasi_isometric X Z
 2. quasi_isometric X Y \<Longrightarrow> quasi_isometric Y X
[PROOF STEP]
assume H: "quasi_isometric X Y"
[PROOF STATE]
proof (state)
this:
quasi_isometric X Y

goal (2 subgoals):
 1. \<lbrakk>quasi_isometric X Y; quasi_isometric Y Z\<rbrakk> \<Longrightarrow> quasi_isometric X Z
 2. quasi_isometric X Y \<Longrightarrow> quasi_isometric Y X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
quasi_isometric X Y
[PROOF STEP]
show "quasi_isometric Y X"
[PROOF STATE]
proof (prove)
using this:
quasi_isometric X Y

goal (1 subgoal):
 1. quasi_isometric Y X
[PROOF STEP]
unfolding quasi_isometric_def
[PROOF STATE]
proof (prove)
using this:
\<exists>lambda C. Ex (lambda C -quasi_isometry_between X Y)

goal (1 subgoal):
 1. \<exists>lambda C. Ex (lambda C -quasi_isometry_between Y X)
[PROOF STEP]
using quasi_isometry_inverse
[PROOF STATE]
proof (prove)
using this:
\<exists>lambda C. Ex (lambda C -quasi_isometry_between X Y)
?lambda ?C -quasi_isometry_between ?X ?Y ?f \<Longrightarrow> \<exists>g. ?lambda (3 * ?C * ?lambda) -quasi_isometry_between ?Y ?X g \<and> (\<forall>x\<in>?X. dist x (g (?f x)) \<le> 3 * ?C * ?lambda) \<and> (\<forall>y\<in>?Y. dist y (?f (g y)) \<le> 3 * ?C * ?lambda)

goal (1 subgoal):
 1. \<exists>lambda C. Ex (lambda C -quasi_isometry_between Y X)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
quasi_isometric Y X

goal (1 subgoal):
 1. \<lbrakk>quasi_isometric X Y; quasi_isometric Y Z\<rbrakk> \<Longrightarrow> quasi_isometric X Z
[PROOF STEP]
assume "quasi_isometric Y Z"
[PROOF STATE]
proof (state)
this:
quasi_isometric Y Z

goal (1 subgoal):
 1. \<lbrakk>quasi_isometric X Y; quasi_isometric Y Z\<rbrakk> \<Longrightarrow> quasi_isometric X Z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
quasi_isometric Y Z
[PROOF STEP]
show "quasi_isometric X Z"
[PROOF STATE]
proof (prove)
using this:
quasi_isometric Y Z

goal (1 subgoal):
 1. quasi_isometric X Z
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
quasi_isometric Y Z
quasi_isometric X Y

goal (1 subgoal):
 1. quasi_isometric X Z
[PROOF STEP]
unfolding quasi_isometric_def
[PROOF STATE]
proof (prove)
using this:
\<exists>lambda C. Ex (lambda C -quasi_isometry_between Y Z)
\<exists>lambda C. Ex (lambda C -quasi_isometry_between X Y)

goal (1 subgoal):
 1. \<exists>lambda C. Ex (lambda C -quasi_isometry_between X Z)
[PROOF STEP]
using quasi_isometry_compose
[PROOF STATE]
proof (prove)
using this:
\<exists>lambda C. Ex (lambda C -quasi_isometry_between Y Z)
\<exists>lambda C. Ex (lambda C -quasi_isometry_between X Y)
\<lbrakk>?lambda ?C -quasi_isometry_between ?X ?Y ?f; ?mu ?D -quasi_isometry_between ?Y ?Z ?g\<rbrakk> \<Longrightarrow> (?lambda * ?mu) (?C * ?mu + 2 * ?D) -quasi_isometry_between ?X ?Z (?g \<circ> ?f)

goal (1 subgoal):
 1. \<exists>lambda C. Ex (lambda C -quasi_isometry_between X Z)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
quasi_isometric X Z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quasi_isometric_empty:
  assumes "X = {}" "quasi_isometric X Y"
  shows "Y = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
X = {}
quasi_isometric X Y

goal (1 subgoal):
 1. Y = {}
[PROOF STEP]
unfolding quasi_isometric_def quasi_isometry_between_def quasi_isometry_on_def
[PROOF STATE]
proof (prove)
using this:
X = {}
\<exists>lambda C f. (1 \<le> lambda \<and> 0 \<le> C \<and> (\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) \<le> lambda * dist x y + C \<and> 1 / lambda * dist x y - C \<le> dist (f x) (f y))) \<and> f ` X \<subseteq> Y \<and> (\<forall>y\<in>Y. \<exists>x\<in>X. dist (f x) y \<le> C)

goal (1 subgoal):
 1. Y = {}
[PROOF STEP]
by blast


[STATEMENT]
lemma quasi_isometric_bounded:
  assumes "bounded X" "quasi_isometric X Y"
  shows "bounded Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded Y
[PROOF STEP]
proof (cases "X = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. X = {} \<Longrightarrow> bounded Y
 2. X \<noteq> {} \<Longrightarrow> bounded Y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
X = {}

goal (2 subgoals):
 1. X = {} \<Longrightarrow> bounded Y
 2. X \<noteq> {} \<Longrightarrow> bounded Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded Y
[PROOF STEP]
using quasi_isometric_empty[OF True assms(2)]
[PROOF STATE]
proof (prove)
using this:
Y = {}

goal (1 subgoal):
 1. bounded Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bounded Y

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> bounded Y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> bounded Y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
X \<noteq> {}

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> bounded Y
[PROOF STEP]
obtain lambda C f where QI: "lambda C-quasi_isometry_between X Y f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>lambda C f. lambda C -quasi_isometry_between X Y f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
quasi_isometric X Y

goal (1 subgoal):
 1. (\<And>lambda C f. lambda C -quasi_isometry_between X Y f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding quasi_isometric_def
[PROOF STATE]
proof (prove)
using this:
\<exists>lambda C. Ex (lambda C -quasi_isometry_between X Y)

goal (1 subgoal):
 1. (\<And>lambda C f. lambda C -quasi_isometry_between X Y f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lambda C -quasi_isometry_between X Y f

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> bounded Y
[PROOF STEP]
obtain x where "x \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
X \<noteq> {}

goal (1 subgoal):
 1. (\<And>x. x \<in> X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> bounded Y
[PROOF STEP]
obtain e where e: "\<And>z. z \<in> X \<Longrightarrow> dist x z \<le> e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e. (\<And>z. z \<in> X \<Longrightarrow> dist x z \<le> e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using bounded_any_center assms(1)
[PROOF STATE]
proof (prove)
using this:
bounded ?S = (\<exists>e. \<forall>y\<in>?S. dist ?a y \<le> e)
bounded X

goal (1 subgoal):
 1. (\<And>e. (\<And>z. z \<in> X \<Longrightarrow> dist x z \<le> e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?z \<in> X \<Longrightarrow> dist x ?z \<le> e

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> bounded Y
[PROOF STEP]
have "dist (f x) y \<le> 2 * C + lambda * e" if "y \<in> Y" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f x) y \<le> 2 * C + lambda * e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (f x) y \<le> 2 * C + lambda * e
[PROOF STEP]
obtain z where *: "z \<in> X" "dist (f z) y \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> X; dist (f z) y \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using quasi_isometry_betweenD(3)[OF QI \<open>y \<in> Y\<close>]
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>X. dist (f x) y \<le> C

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> X; dist (f z) y \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> X
dist (f z) y \<le> C

goal (1 subgoal):
 1. dist (f x) y \<le> 2 * C + lambda * e
[PROOF STEP]
have "dist (f x) y \<le> dist (f x) (f z) + dist (f z) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f x) y \<le> dist (f x) (f z) + dist (f z) y
[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 (f x) y \<le> dist (f x) (f z) + dist (f z) y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (f x) y \<le> dist (f x) (f z) + dist (f z) y

goal (1 subgoal):
 1. dist (f x) y \<le> 2 * C + lambda * e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (f x) y \<le> dist (f x) (f z) + dist (f z) y

goal (1 subgoal):
 1. dist (f x) y \<le> 2 * C + lambda * e
[PROOF STEP]
have "... \<le> (lambda * dist x z + C) + C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f x) (f z) + dist (f z) y \<le> lambda * dist x z + C + C
[PROOF STEP]
using * quasi_isometry_betweenD(4)[OF QI \<open>x \<in> X\<close> \<open>z \<in> X\<close>]
[PROOF STATE]
proof (prove)
using this:
z \<in> X
dist (f z) y \<le> C
dist (f x) (f z) \<le> lambda * dist x z + C

goal (1 subgoal):
 1. dist (f x) (f z) + dist (f z) y \<le> lambda * dist x z + C + C
[PROOF STEP]
by (auto simp add: add_mono)
[PROOF STATE]
proof (state)
this:
dist (f x) (f z) + dist (f z) y \<le> lambda * dist x z + C + C

goal (1 subgoal):
 1. dist (f x) y \<le> 2 * C + lambda * e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (f x) (f z) + dist (f z) y \<le> lambda * dist x z + C + C

goal (1 subgoal):
 1. dist (f x) y \<le> 2 * C + lambda * e
[PROOF STEP]
have "... \<le> 2 * C + lambda * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * dist x z + C + C \<le> 2 * C + lambda * e
[PROOF STEP]
using quasi_isometry_betweenD(6)[OF QI] e[OF \<open>z \<in> X\<close>]
[PROOF STATE]
proof (prove)
using this:
1 \<le> lambda
dist x z \<le> e

goal (1 subgoal):
 1. lambda * dist x z + C + C \<le> 2 * C + lambda * e
[PROOF STEP]
by (auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
lambda * dist x z + C + C \<le> 2 * C + lambda * e

goal (1 subgoal):
 1. dist (f x) y \<le> 2 * C + lambda * e
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (f x) y \<le> 2 * C + lambda * e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (f x) y \<le> 2 * C + lambda * e

goal (1 subgoal):
 1. dist (f x) y \<le> 2 * C + lambda * e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (f x) y \<le> 2 * C + lambda * e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?y \<in> Y \<Longrightarrow> dist (f x) ?y \<le> 2 * C + lambda * e

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> bounded Y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?y \<in> Y \<Longrightarrow> dist (f x) ?y \<le> 2 * C + lambda * e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?y \<in> Y \<Longrightarrow> dist (f x) ?y \<le> 2 * C + lambda * e

goal (1 subgoal):
 1. bounded Y
[PROOF STEP]
unfolding bounded_def
[PROOF STATE]
proof (prove)
using this:
?y \<in> Y \<Longrightarrow> dist (f x) ?y \<le> 2 * C + lambda * e

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quasi_isometric_bounded_iff:
  assumes "bounded X" "X \<noteq> {}" "bounded Y" "Y \<noteq> {}"
  shows "quasi_isometric X Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quasi_isometric X Y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. quasi_isometric X Y
[PROOF STEP]
obtain x y where "x \<in> X" "y \<in> Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> X; y \<in> Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bounded X
X \<noteq> {}
bounded Y
Y \<noteq> {}

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> X; y \<in> Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> X
y \<in> Y

goal (1 subgoal):
 1. quasi_isometric X Y
[PROOF STEP]
obtain C where C: "\<And>z. z \<in> Y \<Longrightarrow> dist y z \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C. (\<And>z. z \<in> Y \<Longrightarrow> dist y z \<le> C) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>bounded Y\<close> bounded_any_center
[PROOF STATE]
proof (prove)
using this:
bounded Y
bounded ?S = (\<exists>e. \<forall>y\<in>?S. dist ?a y \<le> e)

goal (1 subgoal):
 1. (\<And>C. (\<And>z. z \<in> Y \<Longrightarrow> dist y z \<le> C) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?z \<in> Y \<Longrightarrow> dist y ?z \<le> C

goal (1 subgoal):
 1. quasi_isometric X Y
[PROOF STEP]
have "C \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> C
[PROOF STEP]
using C[OF \<open>y \<in> Y\<close>]
[PROOF STATE]
proof (prove)
using this:
dist y y \<le> C

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

goal (1 subgoal):
 1. quasi_isometric X Y
[PROOF STEP]
obtain D where D: "\<And>z. z \<in> X \<Longrightarrow> dist x z \<le> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>D. (\<And>z. z \<in> X \<Longrightarrow> dist x z \<le> D) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>bounded X\<close> bounded_any_center
[PROOF STATE]
proof (prove)
using this:
bounded X
bounded ?S = (\<exists>e. \<forall>y\<in>?S. dist ?a y \<le> e)

goal (1 subgoal):
 1. (\<And>D. (\<And>z. z \<in> X \<Longrightarrow> dist x z \<le> D) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?z \<in> X \<Longrightarrow> dist x ?z \<le> D

goal (1 subgoal):
 1. quasi_isometric X Y
[PROOF STEP]
have "D \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> D
[PROOF STEP]
using D[OF \<open>x \<in> X\<close>]
[PROOF STATE]
proof (prove)
using this:
dist x x \<le> D

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

goal (1 subgoal):
 1. quasi_isometric X Y
[PROOF STEP]
define f::"'a \<Rightarrow> 'b" where "f = (\<lambda>_. y)"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>_. y)

goal (1 subgoal):
 1. quasi_isometric X Y
[PROOF STEP]
have "1 (C + 2 * D)-quasi_isometry_between X Y f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 (C + 2 * D) -quasi_isometry_between X Y f
[PROOF STEP]
proof (rule quasi_isometry_betweenI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 1 (C + 2 * D) -quasi_isometry_on X f
 2. f ` X \<subseteq> Y
 3. \<And>y. y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) y \<le> C + 2 * D
[PROOF STEP]
show "f`X \<subseteq> Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` X \<subseteq> Y
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>_. y) ` X \<subseteq> Y
[PROOF STEP]
using \<open>y \<in> Y\<close>
[PROOF STATE]
proof (prove)
using this:
y \<in> Y

goal (1 subgoal):
 1. (\<lambda>_. y) ` X \<subseteq> Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` X \<subseteq> Y

goal (2 subgoals):
 1. 1 (C + 2 * D) -quasi_isometry_on X f
 2. \<And>y. y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) y \<le> C + 2 * D
[PROOF STEP]
show "1 (C + 2 * D)-quasi_isometry_on X f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 (C + 2 * D) -quasi_isometry_on X f
[PROOF STEP]
proof (rule quasi_isometry_onI, auto simp add: \<open>C \<ge> 0\<close> \<open>D \<ge> 0\<close> f_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist x y \<le> C + 2 * D
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist x y \<le> C + 2 * D
[PROOF STEP]
assume "a \<in> X" "b \<in> X"
[PROOF STATE]
proof (state)
this:
a \<in> X
b \<in> X

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist x y \<le> C + 2 * D
[PROOF STEP]
have "dist a b \<le> dist a x + dist x b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist a b \<le> dist a x + dist x b
[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 a b \<le> dist a x + dist x b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist a b \<le> dist a x + dist x b

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist x y \<le> C + 2 * D
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist a b \<le> dist a x + dist x b

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist x y \<le> C + 2 * D
[PROOF STEP]
have "... \<le> D + D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist a x + dist x b \<le> D + D
[PROOF STEP]
using D[OF \<open>a \<in> X\<close>] D[OF \<open>b \<in> X\<close>]
[PROOF STATE]
proof (prove)
using this:
dist x a \<le> D
dist x b \<le> D

goal (1 subgoal):
 1. dist a x + dist x b \<le> D + D
[PROOF STEP]
by (auto simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist a x + dist x b \<le> D + D

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist x y \<le> C + 2 * D
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist a b \<le> D + D
[PROOF STEP]
show "dist a b \<le> C + 2 * D"
[PROOF STATE]
proof (prove)
using this:
dist a b \<le> D + D

goal (1 subgoal):
 1. dist a b \<le> C + 2 * D
[PROOF STEP]
using \<open>C \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
dist a b \<le> D + D
0 \<le> C

goal (1 subgoal):
 1. dist a b \<le> C + 2 * D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist a b \<le> C + 2 * D

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 (C + 2 * D) -quasi_isometry_on X f

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> \<exists>x\<in>X. dist (f x) y \<le> C + 2 * D
[PROOF STEP]
show "\<exists>a\<in>X. dist (f a) z \<le> C + 2 * D" if "z \<in> Y" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a\<in>X. dist (f a) z \<le> C + 2 * D
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a\<in>X. dist y z \<le> C + 2 * D
[PROOF STEP]
using \<open>x \<in> X\<close> C[OF \<open>z \<in> Y\<close>] \<open>D \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> X
dist y z \<le> C
0 \<le> D

goal (1 subgoal):
 1. \<exists>a\<in>X. dist y z \<le> C + 2 * D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?z \<in> Y \<Longrightarrow> \<exists>a\<in>X. dist (f a) ?z \<le> C + 2 * D

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 (C + 2 * D) -quasi_isometry_between X Y f

goal (1 subgoal):
 1. quasi_isometric X Y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 (C + 2 * D) -quasi_isometry_between X Y f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 (C + 2 * D) -quasi_isometry_between X Y f

goal (1 subgoal):
 1. quasi_isometric X Y
[PROOF STEP]
unfolding quasi_isometric_def
[PROOF STATE]
proof (prove)
using this:
1 (C + 2 * D) -quasi_isometry_between X Y f

goal (1 subgoal):
 1. \<exists>lambda C. Ex (lambda C -quasi_isometry_between X Y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
quasi_isometric X Y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem quasi_isometric_euclidean:
  assumes "quasi_isometric (UNIV::'a::euclidean_space set) (UNIV::'b::euclidean_space set)"
  shows "DIM('a) = DIM('b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DIM('a) = DIM('b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. DIM('a) = DIM('b)
[PROOF STEP]
obtain lambda C and f::"'a \<Rightarrow>'b" where "lambda C-quasi_isometry_on UNIV f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>lambda C f. lambda C -quasi_isometry f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
quasi_isometric UNIV UNIV

goal (1 subgoal):
 1. (\<And>lambda C f. lambda C -quasi_isometry f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding quasi_isometric_def quasi_isometry_between_def
[PROOF STATE]
proof (prove)
using this:
\<exists>lambda C f. lambda C -quasi_isometry f \<and> range f \<subseteq> UNIV \<and> (\<forall>y\<in>UNIV. \<exists>x\<in>UNIV. dist (f x) y \<le> C)

goal (1 subgoal):
 1. (\<And>lambda C f. lambda C -quasi_isometry f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lambda C -quasi_isometry f

goal (1 subgoal):
 1. DIM('a) = DIM('b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lambda C -quasi_isometry f
[PROOF STEP]
have *: "DIM('a) \<le> DIM('b)"
[PROOF STATE]
proof (prove)
using this:
lambda C -quasi_isometry f

goal (1 subgoal):
 1. DIM('a) \<le> DIM('b)
[PROOF STEP]
using quasi_isometry_on_euclidean
[PROOF STATE]
proof (prove)
using this:
lambda C -quasi_isometry f
?lambda ?C -quasi_isometry ?f \<Longrightarrow> DIM(?'a) \<le> DIM(?'b)

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

goal (1 subgoal):
 1. DIM('a) = DIM('b)
[PROOF STEP]
have "quasi_isometric (UNIV::'b::euclidean_space set) (UNIV::'a::euclidean_space set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quasi_isometric UNIV UNIV
[PROOF STEP]
using quasi_isometric_equiv_rel(3)[OF assms]
[PROOF STATE]
proof (prove)
using this:
quasi_isometric UNIV UNIV

goal (1 subgoal):
 1. quasi_isometric UNIV UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
quasi_isometric UNIV UNIV

goal (1 subgoal):
 1. DIM('a) = DIM('b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
quasi_isometric UNIV UNIV
[PROOF STEP]
obtain lambda C and f::"'b \<Rightarrow>'a" where "lambda C-quasi_isometry_on UNIV f"
[PROOF STATE]
proof (prove)
using this:
quasi_isometric UNIV UNIV

goal (1 subgoal):
 1. (\<And>lambda C f. lambda C -quasi_isometry f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding quasi_isometric_def quasi_isometry_between_def
[PROOF STATE]
proof (prove)
using this:
\<exists>lambda C f. lambda C -quasi_isometry f \<and> range f \<subseteq> UNIV \<and> (\<forall>y\<in>UNIV. \<exists>x\<in>UNIV. dist (f x) y \<le> C)

goal (1 subgoal):
 1. (\<And>lambda C f. lambda C -quasi_isometry f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lambda C -quasi_isometry f

goal (1 subgoal):
 1. DIM('a) = DIM('b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lambda C -quasi_isometry f
[PROOF STEP]
have "DIM('b) \<le> DIM('a)"
[PROOF STATE]
proof (prove)
using this:
lambda C -quasi_isometry f

goal (1 subgoal):
 1. DIM('b) \<le> DIM('a)
[PROOF STEP]
using quasi_isometry_on_euclidean
[PROOF STATE]
proof (prove)
using this:
lambda C -quasi_isometry f
?lambda ?C -quasi_isometry ?f \<Longrightarrow> DIM(?'a) \<le> DIM(?'b)

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nb_le_less[iff]: "nb b c \<le> b' \<longleftrightarrow> b < b'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nb b c \<le> b') = (b < b')
[PROOF STEP]
unfolding nb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Abs_contour (c # Rep_contour b) \<le> b') = (b < b')
[PROOF STEP]
by (auto simp add:le_contour_def less_contour_def Rep_contour_inverse Abs_contour_inverse contour_def)


[STATEMENT]
lemma nb_less[iff]: "b' < nb b c \<longleftrightarrow> b' \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b' < nb b c) = (b' \<le> b)
[PROOF STEP]
unfolding nb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b' < Abs_contour (c # Rep_contour b)) = (b' \<le> b)
[PROOF STEP]
by (auto simp add:le_contour_def less_contour_def Rep_contour_inverse Abs_contour_inverse contour_def)


[STATEMENT]
lemma cont2cont_case_lambda [simp, cont2cont]:
  assumes "\<And>a b c. cont (\<lambda>x. f x a b c)"
  shows "cont (\<lambda>x. case_lambda (f x) l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (\<lambda>x. case l of Lambda xa xb xc \<Rightarrow> f x xa xb xc)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cont (\<lambda>x. f x ?a ?b ?c)

goal (1 subgoal):
 1. cont (\<lambda>x. case l of Lambda xa xb xc \<Rightarrow> f x xa xb xc)
[PROOF STEP]
by (cases l) auto


[STATEMENT]
lemma cont2cont_case_d [simp, cont2cont]:
  assumes "\<And>y. cont (\<lambda>x. f1 x y)"
     and  "\<And>y. cont (\<lambda>x. f2 x y)"
     and  "\<And>y. cont (\<lambda>x. f3 x y)"
    and   "cont (\<lambda>x. f4 x)"
  shows "cont (\<lambda>x. case_d (f1 x) (f2 x) (f3 x) (f4 x) d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (\<lambda>x. case d of DI xa \<Rightarrow> f1 x xa | DC xa \<Rightarrow> f2 x xa | DP xa \<Rightarrow> f3 x xa | Stop \<Rightarrow> f4 x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cont (\<lambda>x. f1 x ?y)
cont (\<lambda>x. f2 x ?y)
cont (\<lambda>x. f3 x ?y)
cont f4

goal (1 subgoal):
 1. cont (\<lambda>x. case d of DI xa \<Rightarrow> f1 x xa | DC xa \<Rightarrow> f2 x xa | DP xa \<Rightarrow> f3 x xa | Stop \<Rightarrow> f4 x)
[PROOF STEP]
by (cases d) auto


[STATEMENT]
lemma cont2cont_case_call [simp, cont2cont]:
  assumes "\<And>a b c. cont (\<lambda>x. f1 x a b c)"
     and  "\<And>a b c. cont (\<lambda>x. f2 x a b c)"
  shows "cont (\<lambda>x. case_call (f1 x) (f2 x) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (\<lambda>x. case c of App xa xb xc \<Rightarrow> f1 x xa xb xc | call.Let xa xb xc \<Rightarrow> f2 x xa xb xc)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cont (\<lambda>x. f1 x ?a ?b ?c)
cont (\<lambda>x. f2 x ?a ?b ?c)

goal (1 subgoal):
 1. cont (\<lambda>x. case c of App xa xb xc \<Rightarrow> f1 x xa xb xc | call.Let xa xb xc \<Rightarrow> f2 x xa xb xc)
[PROOF STEP]
by (cases c) auto


[STATEMENT]
lemma cont2cont_case_prim [simp, cont2cont]:
  assumes "\<And>y. cont (\<lambda>x. f1 x y)"
     and  "\<And>y z. cont (\<lambda>x. f2 x y z)"
  shows "cont (\<lambda>x. case_prim (f1 x) (f2 x) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (\<lambda>x. case p of Plus xa \<Rightarrow> f1 x xa | prim.If xa xb \<Rightarrow> f2 x xa xb)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cont (\<lambda>x. f1 x ?y)
cont (\<lambda>x. f2 x ?y ?z)

goal (1 subgoal):
 1. cont (\<lambda>x. case p of Plus xa \<Rightarrow> f1 x xa | prim.If xa xb \<Rightarrow> f2 x xa xb)
[PROOF STEP]
by (cases p) auto


[STATEMENT]
lemma correct_ex1: "\<PR> ex1 = {((2,[1 \<mapsto> \<binit>]), Stop)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<PR> ex1 = {((2, [1 \<mapsto> \<binit>]), Stop)}
[PROOF STEP]
unfolding evalCPS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let ve = Map.empty; \<beta> = Map.empty; f = \<A> (L ex1) \<beta> ve in \<F>\<cdot>(Discr (f, [Stop], ve, \<binit>))) = {((2, [1 \<mapsto> \<binit>]), Stop)}
[PROOF STEP]
by simp


[STATEMENT]
lemma correct_ex2: "\<PR> ex2 = {((2, [1 \<mapsto> \<binit>]), DP (Plus 3)),
                                   ((3, [3 \<mapsto> nb \<binit> 2]),  Stop)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<PR> ex2 = {((2, [1 \<mapsto> \<binit>]), DP (Plus 3)), ((3, [3 \<mapsto> nb \<binit> 2]), Stop)}
[PROOF STEP]
unfolding evalCPS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let ve = Map.empty; \<beta> = Map.empty; f = \<A> (L ex2) \<beta> ve in \<F>\<cdot>(Discr (f, [Stop], ve, \<binit>))) = {((2, [1 \<mapsto> \<binit>]), DP (Plus 3)), ((3, [3 \<mapsto> nb \<binit> 2]), Stop)}
[PROOF STEP]
by simp


[STATEMENT]
lemma tgtasif_inv:
    "\<lbrakk>tgtas u i = Some v; tgtif u i = Some j\<rbrakk> \<Longrightarrow> tgtas v j = Some u"
    "\<lbrakk>tgtas u i = Some v; tgtif u i = Some j\<rbrakk> \<Longrightarrow> tgtif v j = Some i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>tgtas u i = Some v; tgtif u i = Some j\<rbrakk> \<Longrightarrow> tgtas v j = Some u) &&& (\<lbrakk>tgtas u i = Some v; tgtif u i = Some j\<rbrakk> \<Longrightarrow> tgtif v j = Some i)
[PROOF STEP]
by simp+


[STATEMENT]
lemma attr_ifs_valid: "\<lbrakk>ASID y = nF; set ys \<subseteq> hfF_attr\<rbrakk> \<Longrightarrow> d0.ifs_valid (Some y) ys nxt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ASID y = nF; set ys \<subseteq> hfF_attr\<rbrakk> \<Longrightarrow> d0.ifs_valid (Some y) ys nxt
[PROOF STEP]
by(induction ys arbitrary: y)
    (auto simp add: auth_seg0_def leftsegment_wormholed_def attr_segment_def TW.holds_split_tail
                    TW.holds.simps list.case_eq_if)


[STATEMENT]
lemma attr_ifs_valid': "\<lbrakk>set ys \<subseteq> hfF_attr; pre = None\<rbrakk> \<Longrightarrow> d0.ifs_valid pre ys nxt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set ys \<subseteq> hfF_attr; pre = None\<rbrakk> \<Longrightarrow> d0.ifs_valid pre ys nxt
[PROOF STEP]
by(induction ys nxt rule: TW.holds.induct)
    (auto simp add: auth_seg0_def leftsegment_wormholed_def attr_segment_def TW.holds_split_tail
                    TW.holds.simps list.case_eq_if dest: attr_ifs_valid)


[STATEMENT]
lemma leftpath_ifs_valid: "\<lbrakk>pre = None; ASID hf = nF; UpIF hf = Some nE; set xs \<subseteq> hfF_attr\<rbrakk>
    \<Longrightarrow> d0.ifs_valid pre (xs @ [hf, hiEl, hiDl, hiBl, hiAl]) nxt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pre = None; ASID hf = nF; UpIF hf = Some nE; set xs \<subseteq> hfF_attr\<rbrakk> \<Longrightarrow> d0.ifs_valid pre (xs @ [hf, hiEl, hiDr, hiBr, hiAr]) nxt
[PROOF STEP]
by(auto simp add: TW.holds_append auth_seg0_def leftsegment_wormholed_def attr_segment_def
                    TW.holds_split_tail TW.holds.simps list.case_eq_if intro!: attr_ifs_valid')force+


[STATEMENT]
lemma ASM_if_valid: "\<lbrakk>(info, l) \<in> auth_seg0; pre = None\<rbrakk> \<Longrightarrow> d0.ifs_valid pre l nxt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(info, l) \<in> auth_seg0; pre = None\<rbrakk> \<Longrightarrow> d0.ifs_valid pre l nxt
[PROOF STEP]
by(auto simp add: auth_seg0_def leftsegment_wormholed_def attr_segment_def TW.holds_split_tail
                    TW.holds.simps intro: attr_ifs_valid' leftpath_ifs_valid)


[STATEMENT]
lemma rooted_app[simp]: "d0.rooted (xs@y#ys) \<longleftrightarrow> d0.rooted (y#ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d0.rooted (xs @ y # ys) = d0.rooted (y # ys)
[PROOF STEP]
by(induction xs arbitrary: y ys, auto)
    (metis Nil_is_append_conv d0.rooted.simps(2) d0.terminated.cases)+


[STATEMENT]
lemma ASM_rooted: "(info, l) \<in> auth_seg0 \<Longrightarrow> d0.rooted l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (info, l) \<in> auth_seg0 \<Longrightarrow> d0.rooted l
[PROOF STEP]
apply(induction l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (info, []) \<in> auth_seg0 \<Longrightarrow> d0.rooted []
 2. \<And>a l. \<lbrakk>(info, l) \<in> auth_seg0 \<Longrightarrow> d0.rooted l; (info, a # l) \<in> auth_seg0\<rbrakk> \<Longrightarrow> d0.rooted (a # l)
[PROOF STEP]
apply(auto 3 4 simp add: auth_seg0_def leftsegment_wormholed_def attr_segment_def TW.holds_split_tail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>d0.rooted l; ASID a = nF; set l \<subseteq> hfF_attr\<rbrakk> \<Longrightarrow> d0.rooted (a # l)
[PROOF STEP]
subgoal for x xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d0.rooted xs; ASID x = nF; set xs \<subseteq> hfF_attr\<rbrakk> \<Longrightarrow> d0.rooted (x # xs)
[PROOF STEP]
by(cases xs, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ASM_terminated: "(info, l) \<in> auth_seg0 \<Longrightarrow> d0.terminated l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (info, l) \<in> auth_seg0 \<Longrightarrow> d0.terminated l
[PROOF STEP]
apply(auto simp add: auth_seg0_def leftsegment_wormholed_def TW.holds_split_tail attr_segment_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>hf xs. \<lbrakk>info = Num 0; l = xs @ [hf, hiEl, hiDr, hiBr, hiAr]; ASID hf = nF; UpIF hf = Some nE; set xs \<subseteq> hfF_attr\<rbrakk> \<Longrightarrow> d0.terminated (xs @ [hf, hiEl, hiDr, hiBr, hiAr])
 2. set l \<subseteq> hfF_attr \<Longrightarrow> d0.terminated l
[PROOF STEP]
subgoal for hf xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>info = Num 0; l = xs @ [hf, hiEl, hiDr, hiBr, hiAr]; ASID hf = nF; UpIF hf = Some nE; set xs \<subseteq> hfF_attr\<rbrakk> \<Longrightarrow> d0.terminated (xs @ [hf, hiEl, hiDr, hiBr, hiAr])
[PROOF STEP]
by(induction xs, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set l \<subseteq> hfF_attr \<Longrightarrow> d0.terminated l
[PROOF STEP]
by(induction l, auto)


[STATEMENT]
lemma ASM_empty: "(info, []) \<in> auth_seg0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (info, []) \<in> auth_seg0
[PROOF STEP]
by(auto simp add: auth_seg0_def leftsegment_wormholed_def attr_segment_def)


[STATEMENT]
lemma ASM_singleton: "\<lbrakk>ASID hf \<in> bad\<rbrakk> \<Longrightarrow> (info, [hf]) \<in> auth_seg0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASID hf \<in> bad \<Longrightarrow> (info, [hf]) \<in> auth_seg0
[PROOF STEP]
by(auto simp add: auth_seg0_def leftsegment_wormholed_def attr_segment_def)


[STATEMENT]
lemma ASM_extension:
  "\<lbrakk>(info, hf2#ys) \<in> auth_seg0; ASID hf2 \<in> bad; ASID hf1 \<in> bad\<rbrakk>
\<Longrightarrow> (info, hf1#hf2#ys) \<in> auth_seg0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(info, hf2 # ys) \<in> auth_seg0; ASID hf2 \<in> bad; ASID hf1 \<in> bad\<rbrakk> \<Longrightarrow> (info, hf1 # hf2 # ys) \<in> auth_seg0
[PROOF STEP]
by(auto simp add: auth_seg0_def leftsegment_wormholed_def TW.holds_split_tail attr_segment_def)


[STATEMENT]
lemma ASM_modify: "\<lbrakk>(info, hf#ys) \<in> auth_seg0; ASID hf = a;
      ASID hf' = a; UpIF hf' = UpIF hf; a \<in> bad\<rbrakk> \<Longrightarrow> (info, hf'#ys) \<in> auth_seg0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(info, hf # ys) \<in> auth_seg0; ASID hf = a; ASID hf' = a; UpIF hf' = UpIF hf; a \<in> bad\<rbrakk> \<Longrightarrow> (info, hf' # ys) \<in> auth_seg0
[PROOF STEP]
apply(auto simp add: auth_seg0_def leftsegment_wormholed_def attr_segment_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x hfa xs. \<lbrakk>ASID hf = nF; ASID hf' = nF; UpIF hf' = UpIF hf; a = nF; x \<in> set ys; info = Num 0; hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr; ASID x \<noteq> nF; \<forall>hf. UpIF hf = Some nE \<longrightarrow> ASID hf = nF \<longrightarrow> (\<forall>xs. hf' # ys = xs @ [hf, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr)\<rbrakk> \<Longrightarrow> hf' = hiGr
 2. \<And>x hfa xs. \<lbrakk>ASID hf = nF; ASID hf' = nF; UpIF hf' = UpIF hf; a = nF; x \<in> set ys; info = Num 0; hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr; ASID x \<noteq> nF; \<forall>hf. UpIF hf = Some nE \<longrightarrow> ASID hf = nF \<longrightarrow> (\<forall>xs. hf' # ys = xs @ [hf, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr)\<rbrakk> \<Longrightarrow> ys = [hiEr, hiDr, hiBr, hiAr]
[PROOF STEP]
subgoal for y hfa l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ASID hf = nF; ASID hf' = nF; UpIF hf' = UpIF hf; a = nF; y \<in> set ys; info = Num 0; hf # ys = l @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set l \<subseteq> hfF_attr; ASID y \<noteq> nF; \<forall>hf. UpIF hf = Some nE \<longrightarrow> ASID hf = nF \<longrightarrow> (\<forall>xs. hf' # ys = xs @ [hf, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr)\<rbrakk> \<Longrightarrow> hf' = hiGr
[PROOF STEP]
by(induction l, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x hfa xs. \<lbrakk>ASID hf = nF; ASID hf' = nF; UpIF hf' = UpIF hf; a = nF; x \<in> set ys; info = Num 0; hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr; ASID x \<noteq> nF; \<forall>hf. UpIF hf = Some nE \<longrightarrow> ASID hf = nF \<longrightarrow> (\<forall>xs. hf' # ys = xs @ [hf, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr)\<rbrakk> \<Longrightarrow> ys = [hiEr, hiDr, hiBr, hiAr]
[PROOF STEP]
subgoal for y hfa l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ASID hf = nF; ASID hf' = nF; UpIF hf' = UpIF hf; a = nF; y \<in> set ys; info = Num 0; hf # ys = l @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set l \<subseteq> hfF_attr; ASID y \<noteq> nF; \<forall>hf. UpIF hf = Some nE \<longrightarrow> ASID hf = nF \<longrightarrow> (\<forall>xs. hf' # ys = xs @ [hf, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr)\<rbrakk> \<Longrightarrow> ys = [hiEr, hiDr, hiBr, hiAr]
[PROOF STEP]
by(induction l, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rightpath_no_nF: "\<lbrakk>ASID hf = nF; zs @ hf # ys = rightpath\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ASID hf = nF; zs @ hf # ys = rightpath\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(cases ys rule: rev_cases, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ysa. \<lbrakk>ASID hf = nF; zs @ hf # ysa = [hiGr, hiEr, hiDr, hiBr]; ys = ysa @ [hiAr]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for ys'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ASID hf = nF; zs @ hf # ys' = [hiGr, hiEr, hiDr, hiBr]; ys = ys' @ [hiAr]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(cases ys' rule: rev_cases, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ysa. \<lbrakk>ASID hf = nF; zs @ hf # ysa = [hiGr, hiEr, hiDr]; ys = ysa @ [hiBr, hiAr]; ys' = ysa @ [hiBr]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for ys''
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ASID hf = nF; zs @ hf # ys'' = [hiGr, hiEr, hiDr]; ys = ys'' @ [hiBr, hiAr]; ys' = ys'' @ [hiBr]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(cases ys'' rule: rev_cases, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ysa. \<lbrakk>ASID hf = nF; zs @ hf # ysa = [hiGr, hiEr]; ys = ysa @ [hiDr, hiBr, hiAr]; ys' = ysa @ [hiDr, hiBr]; ys'' = ysa @ [hiDr]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for ys'''
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ASID hf = nF; zs @ hf # ys''' = [hiGr, hiEr]; ys = ys''' @ [hiDr, hiBr, hiAr]; ys' = ys''' @ [hiDr, hiBr]; ys'' = ys''' @ [hiDr]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(cases ys''' rule: rev_cases, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ysa. \<lbrakk>ASID hf = nF; zs @ hf # ysa = [hiGr]; ys = ysa @ [hiEr, hiDr, hiBr, hiAr]; ys' = ysa @ [hiEr, hiDr, hiBr]; ys'' = ysa @ [hiEr, hiDr]; ys''' = ysa @ [hiEr]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for ys'''
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ASID hf = nF; zs @ hf # ys''' = [hiGr]; ys = ys''' @ [hiEr, hiDr, hiBr, hiAr]; ys' = ys''' @ [hiEr, hiDr, hiBr]; ys'' = ys''' @ [hiEr, hiDr]; ys'''__ = ys''' @ [hiEr]\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by(cases ys''' rule: rev_cases, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ASM_cutoff_leftpath:
"\<lbrakk>ASID hf = nF;
\<forall>hfa. UpIF hfa = Some nE \<longrightarrow> ASID hfa = nF \<longrightarrow> (\<forall>xs. hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr] \<longrightarrow>
\<not> set xs \<subseteq> hfF_attr); x \<in> set ys; info = Num 0;
        zs @ hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr\<rbrakk>
       \<Longrightarrow> ASID x = nF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ASID hf = nF; \<forall>hfa. UpIF hfa = Some nE \<longrightarrow> ASID hfa = nF \<longrightarrow> (\<forall>xs. hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr); x \<in> set ys; info = Num 0; zs @ hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr\<rbrakk> \<Longrightarrow> ASID x = nF
[PROOF STEP]
apply(cases ys rule: rev_cases, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ysa y. \<lbrakk>ASID hf = nF; \<forall>hfa. UpIF hfa = Some nE \<longrightarrow> ASID hfa = nF \<longrightarrow> (\<forall>xs. hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr); x \<in> set ys; info = Num 0; zs @ hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr; ys = ysa @ [y]\<rbrakk> \<Longrightarrow> ASID x = nF
[PROOF STEP]
subgoal for ys' b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ASID hf = nF; \<forall>hfa. UpIF hfa = Some nE \<longrightarrow> ASID hfa = nF \<longrightarrow> (\<forall>xs. hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr); x \<in> set ys; info = Num 0; zs @ hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr; ys = ys' @ [b]\<rbrakk> \<Longrightarrow> ASID x = nF
[PROOF STEP]
apply(cases ys' rule: rev_cases, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ysa y. \<lbrakk>ASID hf = nF; \<forall>hfa. UpIF hfa = Some nE \<longrightarrow> ASID hfa = nF \<longrightarrow> (\<forall>xs. hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr); x \<in> set ys; info = Num 0; zs @ hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr; ys = ys' @ [b]; ys' = ysa @ [y]\<rbrakk> \<Longrightarrow> ASID x = nF
[PROOF STEP]
subgoal for ys'' c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ASID hf = nF; \<forall>hfa. UpIF hfa = Some nE \<longrightarrow> ASID hfa = nF \<longrightarrow> (\<forall>xs. hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr); x \<in> set ys; info = Num 0; zs @ hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr; ys = ys' @ [b]; ys' = ys'' @ [c]\<rbrakk> \<Longrightarrow> ASID x = nF
[PROOF STEP]
apply(cases ys'' rule: rev_cases, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ysa y. \<lbrakk>ASID hf = nF; \<forall>hfa. UpIF hfa = Some nE \<longrightarrow> ASID hfa = nF \<longrightarrow> (\<forall>xs. hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr); x \<in> set ys; info = Num 0; zs @ hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr; ys = ys' @ [b]; ys' = ys'' @ [c]; ys'' = ysa @ [y]\<rbrakk> \<Longrightarrow> ASID x = nF
[PROOF STEP]
subgoal for ys''' d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ASID hf = nF; \<forall>hfa. UpIF hfa = Some nE \<longrightarrow> ASID hfa = nF \<longrightarrow> (\<forall>xs. hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr); x \<in> set ys; info = Num 0; zs @ hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr; ys = ys' @ [b]; ys' = ys'' @ [c]; ys'' = ys''' @ [d]\<rbrakk> \<Longrightarrow> ASID x = nF
[PROOF STEP]
apply(cases ys'' rule: rev_cases, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ysa y. \<lbrakk>ASID hf = nF; \<forall>hfa. UpIF hfa = Some nE \<longrightarrow> ASID hfa = nF \<longrightarrow> (\<forall>xs. hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr); x \<in> set ys; info = Num 0; zs @ hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr; ys = ys' @ [b]; ys' = ys'' @ [c]; ys'' = ys''' @ [d]; ys'' = ysa @ [y]\<rbrakk> \<Longrightarrow> ASID x = nF
[PROOF STEP]
subgoal for ys''' e
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ASID hf = nF; \<forall>hfa. UpIF hfa = Some nE \<longrightarrow> ASID hfa = nF \<longrightarrow> (\<forall>xs. hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr); x \<in> set ys; info = Num 0; zs @ hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr; ys = ys' @ [b]; ys' = ys'' @ [c]; ys'' = ys'''__ @ [d]; ys'' = ys''' @ [e]\<rbrakk> \<Longrightarrow> ASID x = nF
[PROOF STEP]
apply(cases ys''' rule: rev_cases, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ysa y. \<lbrakk>ASID hf = nF; \<forall>hfa. UpIF hfa = Some nE \<longrightarrow> ASID hfa = nF \<longrightarrow> (\<forall>xs. hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr); x \<in> set ys; info = Num 0; zs @ hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr; ys = ys' @ [b]; ys' = ys'' @ [c]; ys'' = ys'''__ @ [d]; ys'' = ys''' @ [e]; ys''' = ysa @ [y]\<rbrakk> \<Longrightarrow> ASID x = nF
[PROOF STEP]
subgoal for ys'''' f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ASID hf = nF; \<forall>hfa. UpIF hfa = Some nE \<longrightarrow> ASID hfa = nF \<longrightarrow> (\<forall>xs. hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr); x \<in> set ys; info = Num 0; zs @ hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr; ys = ys' @ [b]; ys' = ys'' @ [c]; ys'' = ys'''__ @ [d]; ys'' = ys''' @ [e]; ys''' = ys'''' @ [f]\<rbrakk> \<Longrightarrow> ASID x = nF
[PROOF STEP]
apply(cases ys'''' rule: rev_cases, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ASID hf = nF; \<forall>hfa. UpIF hfa = Some nE \<longrightarrow> ASID hfa = nF \<longrightarrow> (\<forall>xs. hf # ys'''__ = xs @ [hfa, hiEl] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr); x = hiDr \<or> x = hiBr \<or> x = hiAr \<or> x \<in> set ys'''__; info = Num 0; zs @ hf # ys'''__ = xs @ [hfa, hiEl] \<and> d = hiDr \<and> c = hiBr \<and> b = hiAr; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr; ys = ys'''__ @ [hiDr, hiBr, hiAr]; ys' = ys'''__ @ [hiDr, hiBr]; [f] = ys'''__ \<and> e = hiDr; ys'' = ys'''__ @ [hiDr]; ys''' = ys'''__; ys'''' = []\<rbrakk> \<Longrightarrow> ASID x = nF
 2. \<And>ysa y. \<lbrakk>ASID hf = nF; \<forall>hfa. UpIF hfa = Some nE \<longrightarrow> ASID hfa = nF \<longrightarrow> (\<forall>xs. hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr] \<longrightarrow> \<not> set xs \<subseteq> hfF_attr); x \<in> set ys; info = Num 0; zs @ hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs \<subseteq> hfF_attr; ys = ys' @ [b]; ys' = ys'' @ [c]; ys'' = ys'''__ @ [d]; ys'' = ys''' @ [e]; ys''' = ys'''' @ [f]; ys'''' = ysa @ [y]\<rbrakk> \<Longrightarrow> ASID x = nF
[PROOF STEP]
by auto blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ASM_cutoff: "\<lbrakk>(info, zs@hf#ys) \<in> auth_seg0; ASID hf \<in> bad\<rbrakk> \<Longrightarrow> (info, hf#ys) \<in> auth_seg0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(info, zs @ hf # ys) \<in> auth_seg0; ASID hf \<in> bad\<rbrakk> \<Longrightarrow> (info, hf # ys) \<in> auth_seg0
[PROOF STEP]
apply(simp add: auth_seg0_def, auto dest: rightpath_no_nF)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>ASID hf = nF; (info, hf # ys) \<notin> attr_segment; (info, zs @ hf # ys) \<in> leftsegment_wormholed; (info, hf # ys) \<notin> leftsegment_wormholed\<rbrakk> \<Longrightarrow> info = Num 0
 2. \<lbrakk>ASID hf = nF; (info, hf # ys) \<notin> attr_segment; (info, zs @ hf # ys) \<in> leftsegment_wormholed; (info, hf # ys) \<notin> leftsegment_wormholed\<rbrakk> \<Longrightarrow> hf = hiGr
 3. \<lbrakk>ASID hf = nF; (info, hf # ys) \<notin> attr_segment; (info, zs @ hf # ys) \<in> leftsegment_wormholed; (info, hf # ys) \<notin> leftsegment_wormholed\<rbrakk> \<Longrightarrow> ys = [hiEr, hiDr, hiBr, hiAr]
 4. \<lbrakk>ASID hf = nF; (info, hf # ys) \<notin> attr_segment; (info, zs @ hf # ys) \<in> attr_segment; (info, hf # ys) \<notin> leftsegment_wormholed\<rbrakk> \<Longrightarrow> info = Num 0
 5. \<lbrakk>ASID hf = nF; (info, hf # ys) \<notin> attr_segment; (info, zs @ hf # ys) \<in> attr_segment; (info, hf # ys) \<notin> leftsegment_wormholed\<rbrakk> \<Longrightarrow> hf = hiGr
 6. \<lbrakk>ASID hf = nF; (info, hf # ys) \<notin> attr_segment; (info, zs @ hf # ys) \<in> attr_segment; (info, hf # ys) \<notin> leftsegment_wormholed\<rbrakk> \<Longrightarrow> ys = [hiEr, hiDr, hiBr, hiAr]
[PROOF STEP]
by(auto simp add: leftsegment_wormholed_def TW.holds_split_tail attr_segment_def intro: ASM_cutoff_leftpath)


[STATEMENT]
lemma "e1.hf_valid ainfo uinfo hfAl None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1.hf_valid (Num 0) 1 hfAl None
[PROOF STEP]
by (simp add: e1.hf_valid_invert hfAl_def)


[STATEMENT]
lemma "e1.hf_valid ainfo uinfo hfBl (Some hfAl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1.hf_valid (Num 0) 1 hfBl (Some hfAl)
[PROOF STEP]
apply (auto simp add: e1.hf_valid_invert hfAl_def hfBl_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Ex (d0.ASIF (Some nB))
 2. Ex (d0.ASIF None)
[PROOF STEP]
using d0.ASIF.simps
[PROOF STATE]
proof (prove)
using this:
d0.ASIF (Some ?a) (AS ?a') = (?a = ?a')
d0.ASIF None \<epsilon> = True
d0.ASIF None (AS ?v) = False
d0.ASIF None (Num ?v) = False
d0.ASIF None (Key ?va) = False
d0.ASIF None (Nonce ?vd) = False
d0.ASIF None (L ?vc) = False
d0.ASIF None (FS ?vb) = False
d0.ASIF None \<langle>?ve, ?vaa\<rangle> = False
d0.ASIF None (Hash ?ve) = False
d0.ASIF None (Crypt ?va ?vaa) = False
d0.ASIF (Some ?v) \<epsilon> = False
d0.ASIF ?uu (Num ?v) = False
d0.ASIF ?uu (Key ?va) = False
d0.ASIF ?uu (Nonce ?vd) = False
d0.ASIF ?uu (L ?vc) = False
d0.ASIF ?uu (FS ?vb) = False
d0.ASIF ?uu \<langle>?ve, ?vaa\<rangle> = False
d0.ASIF ?uu (Hash ?ve) = False
d0.ASIF ?uu (Crypt ?va ?vaa) = False

goal (2 subgoals):
 1. Ex (d0.ASIF (Some nB))
 2. Ex (d0.ASIF None)
[PROOF STEP]
by blast+


[STATEMENT]
lemma "e1.hf_valid ainfo uinfo hfFl (Some hfEl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1.hf_valid (Num 0) 1 hfFl (Some hfEl)
[PROOF STEP]
apply (auto intro!: exI simp add: e1.hf_valid_invert hfl_defs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. d0.ASIF (Some nF) ?x2
 2. d0.ASIF (Some nD) ?x3
[PROOF STEP]
using d0.ASIF.simps
[PROOF STATE]
proof (prove)
using this:
d0.ASIF (Some ?a) (AS ?a') = (?a = ?a')
d0.ASIF None \<epsilon> = True
d0.ASIF None (AS ?v) = False
d0.ASIF None (Num ?v) = False
d0.ASIF None (Key ?va) = False
d0.ASIF None (Nonce ?vd) = False
d0.ASIF None (L ?vc) = False
d0.ASIF None (FS ?vb) = False
d0.ASIF None \<langle>?ve, ?vaa\<rangle> = False
d0.ASIF None (Hash ?ve) = False
d0.ASIF None (Crypt ?va ?vaa) = False
d0.ASIF (Some ?v) \<epsilon> = False
d0.ASIF ?uu (Num ?v) = False
d0.ASIF ?uu (Key ?va) = False
d0.ASIF ?uu (Nonce ?vd) = False
d0.ASIF ?uu (L ?vc) = False
d0.ASIF ?uu (FS ?vb) = False
d0.ASIF ?uu \<langle>?ve, ?vaa\<rangle> = False
d0.ASIF ?uu (Hash ?ve) = False
d0.ASIF ?uu (Crypt ?va ?vaa) = False

goal (2 subgoals):
 1. d0.ASIF (Some nF) ?x2
 2. d0.ASIF (Some nD) ?x3
[PROOF STEP]
by blast+


[STATEMENT]
lemma forwardingpath_valid: "e1.hfs_valid_None ainfo uinfo forwardingpath"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1.hfs_valid_None (Num 0) 1 [hfFl, hfEl, hfDl, hfBl, hfAl]
[PROOF STEP]
by(auto simp add: TWu.holds_split_tail hfl_defs)


[STATEMENT]
lemma forwardingpath_auth: "pfragment ainfo forwardingpath (e1.auth_seg2 uinfo)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pfragment (Num 0) [hfFl, hfEl, hfDl, hfBl, hfAl] (e1.auth_seg2 1)
[PROOF STEP]
apply(auto simp add: e1.auth_seg2_def pfragment_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>zs1 zs2. e1.hfs_valid_prefix_generic (Num 0) (Suc 0) [] None (zs1 @ hfFl # hfEl # hfDl # hfBl # hfAl # zs2) None = zs1 @ hfFl # hfEl # hfDl # hfBl # hfAl # zs2 \<and> (Num 0, map AHI zs1 @ AHI hfFl # AHI hfEl # AHI hfDl # AHI hfBl # AHI hfAl # map AHI zs2) \<in> auth_seg0
[PROOF STEP]
using forwardingpath_valid
[PROOF STATE]
proof (prove)
using this:
e1.hfs_valid_None (Num 0) 1 [hfFl, hfEl, hfDl, hfBl, hfAl]

goal (1 subgoal):
 1. \<exists>zs1 zs2. e1.hfs_valid_prefix_generic (Num 0) (Suc 0) [] None (zs1 @ hfFl # hfEl # hfDl # hfBl # hfAl # zs2) None = zs1 @ hfFl # hfEl # hfDl # hfBl # hfAl # zs2 \<and> (Num 0, map AHI zs1 @ AHI hfFl # AHI hfEl # AHI hfDl # AHI hfBl # AHI hfAl # map AHI zs2) \<in> auth_seg0
[PROOF STEP]
by(auto intro!: exI[of _ "[]"] simp add: e1.hfs_valid_prefix_generic_def auth_seg0_def leftsegment_wormholed_def hfl_defs)


[STATEMENT]
lemma reach_s0: "reach e1.dp2 s0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach e1.dp2 s0
[PROOF STEP]
by(auto simp add: s0_def e1.dp2_def)


[STATEMENT]
lemma s0_s1: "e1.dp2: s0 \<midarrow>evt_dispatch_int2 nF pkt0\<rightarrow> s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1.dp2: s0\<midarrow>evt_dispatch_int2 nF pkt0\<rightarrow> s1
[PROOF STEP]
using forwardingpath_auth
[PROOF STATE]
proof (prove)
using this:
pfragment (Num 0) [hfFl, hfEl, hfDl, hfBl, hfAl] (e1.auth_seg2 1)

goal (1 subgoal):
 1. e1.dp2: s0\<midarrow>evt_dispatch_int2 nF pkt0\<rightarrow> s1
[PROOF STEP]
by(auto dest!: e1.dp2_dispatch_int_also_works_for_honest[where ?m = pkt0])
    (auto simp add: e1.dp2_def e1.dp2_defs e1.dp2_msgs forwading_states pkt0_def e1.dp2_init_def)


[STATEMENT]
lemma s1_s2: "e1.dp2: s1 \<midarrow>evt_send2 nF nE pkt0\<rightarrow> s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1.dp2: s1\<midarrow>evt_send2 nF nE pkt0\<rightarrow> s2
[PROOF STEP]
by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt0_def pkt1_def)
     (auto simp add: hfl_defs)


[STATEMENT]
lemma s2_s3: "e1.dp2: s2 \<midarrow>evt_recv2 nE nF pkt1\<rightarrow> s3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1.dp2: s2\<midarrow>evt_recv2 nE nF pkt1\<rightarrow> s3
[PROOF STEP]
by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt0_def pkt1_def)
     (auto simp add: hfl_defs)


[STATEMENT]
lemma s3_s4: "e1.dp2: s3 \<midarrow>evt_send2 nE nD pkt1\<rightarrow> s4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1.dp2: s3\<midarrow>evt_send2 nE nD pkt1\<rightarrow> s4
[PROOF STEP]
by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt1_def pkt2_def)
     (auto simp add: hfl_defs)


[STATEMENT]
lemma s4_s5: "e1.dp2: s4 \<midarrow>evt_recv2 nD nE pkt2\<rightarrow> s5"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1.dp2: s4\<midarrow>evt_recv2 nD nE pkt2\<rightarrow> s5
[PROOF STEP]
by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt1_def pkt2_def)
     (auto simp add: hfl_defs)


[STATEMENT]
lemma s5_s6: "e1.dp2: s5 \<midarrow>evt_send2 nD nB pkt2\<rightarrow> s6"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1.dp2: s5\<midarrow>evt_send2 nD nB pkt2\<rightarrow> s6
[PROOF STEP]
by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt3_def pkt2_def)
     (auto simp add: hfl_defs)


[STATEMENT]
lemma s6_s7: "e1.dp2: s6 \<midarrow>evt_recv2 nB nD pkt3\<rightarrow> s7"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1.dp2: s6\<midarrow>evt_recv2 nB nD pkt3\<rightarrow> s7
[PROOF STEP]
by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt3_def pkt2_def)
     (auto simp add: hfl_defs)


[STATEMENT]
lemma s7_s8: "e1.dp2: s7 \<midarrow>evt_send2 nB nA pkt3\<rightarrow> s8"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1.dp2: s7\<midarrow>evt_send2 nB nA pkt3\<rightarrow> s8
[PROOF STEP]
by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt4_def pkt3_def)
     (auto simp add: hfl_defs)


[STATEMENT]
lemma s8_s9: "e1.dp2: s8 \<midarrow>evt_recv2 nA nB pkt4\<rightarrow> s9"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1.dp2: s8\<midarrow>evt_recv2 nA nB pkt4\<rightarrow> s9
[PROOF STEP]
by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt4_def pkt3_def)
     (auto simp add: hfl_defs)


[STATEMENT]
lemma s9_s10: "e1.dp2: s9 \<midarrow>evt_deliver2 nA pkt4\<rightarrow> s10"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1.dp2: s9\<midarrow>evt_deliver2 nA pkt4\<rightarrow> s10
[PROOF STEP]
by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt5_def pkt4_def)
     (auto simp add: hfl_defs)


[STATEMENT]
lemma executability: "reach e1.dp2 s10"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach e1.dp2 s10
[PROOF STEP]
using reach_s0 s0_s1 s1_s2 s2_s3 s3_s4 s4_s5 s5_s6 s6_s7 s7_s8 s8_s9 s9_s10
[PROOF STATE]
proof (prove)
using this:
reach e1.dp2 s0
e1.dp2: s0\<midarrow>evt_dispatch_int2 nF pkt0\<rightarrow> s1
e1.dp2: s1\<midarrow>evt_send2 nF nE pkt0\<rightarrow> s2
e1.dp2: s2\<midarrow>evt_recv2 nE nF pkt1\<rightarrow> s3
e1.dp2: s3\<midarrow>evt_send2 nE nD pkt1\<rightarrow> s4
e1.dp2: s4\<midarrow>evt_recv2 nD nE pkt2\<rightarrow> s5
e1.dp2: s5\<midarrow>evt_send2 nD nB pkt2\<rightarrow> s6
e1.dp2: s6\<midarrow>evt_recv2 nB nD pkt3\<rightarrow> s7
e1.dp2: s7\<midarrow>evt_send2 nB nA pkt3\<rightarrow> s8
e1.dp2: s8\<midarrow>evt_recv2 nA nB pkt4\<rightarrow> s9
e1.dp2: s9\<midarrow>evt_deliver2 nA pkt4\<rightarrow> s10

goal (1 subgoal):
 1. reach e1.dp2 s10
[PROOF STEP]
by(auto elim!: reach_trans)


[STATEMENT]
lemma ik_hfs_in_ik: "t \<in> e1.ik_hfs \<Longrightarrow> t \<in> synth (analz (e1.ik_dyn s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> e1.ik_hfs \<Longrightarrow> t \<in> synth (analz (e1.ik_dyn s))
[PROOF STEP]
by(auto simp add: e1.ik_dyn_def e1.ik_def)


[STATEMENT]
lemma hvf_e_auth: "HVF hfEl \<in> e1.ik_hfs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HVF hfEl \<in> e1.ik_hfs
[PROOF STEP]
apply(auto simp add: e1.ik_hfs_def e1.auth_seg2_def
               intro!: exI[of _ hfEl] exI[of _ "[hfFl, hfEl, hfDl, hfBl, hfAl]"] exI[of _ ainfo])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>uinfo. e1.hfs_valid_prefix_generic (Num 0) uinfo [] None [hfFl, hfEl, hfDl, hfBl, hfAl] None = [hfFl, hfEl, hfDl, hfBl, hfAl]
 2. (Num 0, [AHI hfFl, AHI hfEl, AHI hfDl, AHI hfBl, AHI hfAl]) \<in> auth_seg0
[PROOF STEP]
using e1.hfs_valid_prefix_generic_def no_assumptions_left.forwardingpath_valid
[PROOF STATE]
proof (prove)
using this:
e1.hfs_valid_prefix_generic ?ainfo ?uinfo ?pas ?pre ?fut ?nxt \<equiv> e1.hfs_valid_prefix ?ainfo ?uinfo ?fut ?nxt
e1.hfs_valid_None (Num 0) 1 [hfFl, hfEl, hfDl, hfBl, hfAl]

goal (2 subgoals):
 1. \<exists>uinfo. e1.hfs_valid_prefix_generic (Num 0) uinfo [] None [hfFl, hfEl, hfDl, hfBl, hfAl] None = [hfFl, hfEl, hfDl, hfBl, hfAl]
 2. (Num 0, [AHI hfFl, AHI hfEl, AHI hfDl, AHI hfBl, AHI hfAl]) \<in> auth_seg0
[PROOF STEP]
by(auto intro!: exI[of _ uinfo] simp add: auth_seg0_def leftsegment_wormholed_def hfl_defs)


[STATEMENT]
lemma uhi_e_auth: "UHI hfEl \<in> e1.ik_hfs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UHI hfEl \<in> e1.ik_hfs
[PROOF STEP]
apply(auto simp add: e1.ik_hfs_def e1.auth_seg2_def
               intro!: exI[of _ hfEl] exI[of _ "[hfFl, hfEl, hfDl, hfBl, hfAl]"] exI[of _ ainfo])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>uinfo. e1.hfs_valid_prefix_generic (Num 0) uinfo [] None [hfFl, hfEl, hfDl, hfBl, hfAl] None = [hfFl, hfEl, hfDl, hfBl, hfAl]
 2. (Num 0, [AHI hfFl, AHI hfEl, AHI hfDl, AHI hfBl, AHI hfAl]) \<in> auth_seg0
[PROOF STEP]
using e1.hfs_valid_prefix_generic_def no_assumptions_left.forwardingpath_valid
[PROOF STATE]
proof (prove)
using this:
e1.hfs_valid_prefix_generic ?ainfo ?uinfo ?pas ?pre ?fut ?nxt \<equiv> e1.hfs_valid_prefix ?ainfo ?uinfo ?fut ?nxt
e1.hfs_valid_None (Num 0) 1 [hfFl, hfEl, hfDl, hfBl, hfAl]

goal (2 subgoals):
 1. \<exists>uinfo. e1.hfs_valid_prefix_generic (Num 0) uinfo [] None [hfFl, hfEl, hfDl, hfBl, hfAl] None = [hfFl, hfEl, hfDl, hfBl, hfAl]
 2. (Num 0, [AHI hfFl, AHI hfEl, AHI hfDl, AHI hfBl, AHI hfAl]) \<in> auth_seg0
[PROOF STEP]
by(auto simp add: e1.auth_seg2_def auth_seg0_def leftsegment_wormholed_def hfl_defs)


[STATEMENT]
lemma attr_executability: "reach e1.dp2 s_attr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach e1.dp2 s_attr
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. reach e1.dp2 s_attr
[PROOF STEP]
have "e1.dp2: s0 \<midarrow>evt_dispatch_ext2 nF nE pkt_attr\<rightarrow> s_attr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1.dp2: s0\<midarrow>evt_dispatch_ext2 nF nE pkt_attr\<rightarrow> s_attr
[PROOF STEP]
apply (auto simp add: forwading_states e1.dp2_defs e1.dp2_msgs pkt_attr_def e1.ik_hfs_def e1.terms_pkt_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. HVF hfEl \<in> synth (analz (e1.ik_dyn \<lparr>chan2 = \<lambda>_. {}, loc2 = \<lambda>_. {}\<rparr>))
 2. UHI hfEl \<in> synth (analz (e1.ik_dyn \<lparr>chan2 = \<lambda>_. {}, loc2 = \<lambda>_. {}\<rparr>))
 3. s_attr = \<lparr>chan2 = (\<lambda>_. {})((nF, nE, nE, nF) := {\<lparr>pkt2.AInfo = Num 0, UInfo = Suc 0, past = [], future = [hfEl], history = []\<rparr>}), loc2 = \<lambda>_. {}\<rparr>
[PROOF STEP]
using hvf_e_auth uhi_e_auth
[PROOF STATE]
proof (prove)
using this:
HVF hfEl \<in> e1.ik_hfs
UHI hfEl \<in> e1.ik_hfs

goal (3 subgoals):
 1. HVF hfEl \<in> synth (analz (e1.ik_dyn \<lparr>chan2 = \<lambda>_. {}, loc2 = \<lambda>_. {}\<rparr>))
 2. UHI hfEl \<in> synth (analz (e1.ik_dyn \<lparr>chan2 = \<lambda>_. {}, loc2 = \<lambda>_. {}\<rparr>))
 3. s_attr = \<lparr>chan2 = (\<lambda>_. {})((nF, nE, nE, nF) := {\<lparr>pkt2.AInfo = Num 0, UInfo = Suc 0, past = [], future = [hfEl], history = []\<rparr>}), loc2 = \<lambda>_. {}\<rparr>
[PROOF STEP]
by(auto dest: ik_hfs_in_ik simp add: s_attr_def s0_def e1.dp2_init_def pkt_attr_def)
[PROOF STATE]
proof (state)
this:
e1.dp2: s0\<midarrow>evt_dispatch_ext2 nF nE pkt_attr\<rightarrow> s_attr

goal (1 subgoal):
 1. reach e1.dp2 s_attr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e1.dp2: s0\<midarrow>evt_dispatch_ext2 nF nE pkt_attr\<rightarrow> s_attr
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
e1.dp2: s0\<midarrow>evt_dispatch_ext2 nF nE pkt_attr\<rightarrow> s_attr

goal (1 subgoal):
 1. reach e1.dp2 s_attr
[PROOF STEP]
using reach_s0
[PROOF STATE]
proof (prove)
using this:
e1.dp2: s0\<midarrow>evt_dispatch_ext2 nF nE pkt_attr\<rightarrow> s_attr
reach e1.dp2 s0

goal (1 subgoal):
 1. reach e1.dp2 s_attr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reach e1.dp2 s_attr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem set_inter_compl_diff [simp]: \<open>- A \<inter> B = B - A\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - A \<inter> B = B - A
[PROOF STEP]
by blast


[STATEMENT]
theorem closedt_mono: assumes le: \<open>i \<le> j\<close>
  shows \<open>closedt i (t::'a term) \<Longrightarrow> closedt j t\<close>
    and \<open>closedts i (ts::'a term list) \<Longrightarrow> closedts j ts\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (closedt i t \<Longrightarrow> closedt j t) &&& (closedts i ts \<Longrightarrow> closedts j ts)
[PROOF STEP]
using le
[PROOF STATE]
proof (prove)
using this:
i \<le> j

goal (1 subgoal):
 1. (closedt i t \<Longrightarrow> closedt j t) &&& (closedts i ts \<Longrightarrow> closedts j ts)
[PROOF STEP]
by (induct t and ts rule: closedt.induct closedts.induct) simp_all


[STATEMENT]
theorem closed_mono: assumes le: \<open>i \<le> j\<close>
  shows \<open>closed i p \<Longrightarrow> closed j p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed i p \<Longrightarrow> closed j p
[PROOF STEP]
using le
[PROOF STATE]
proof (prove)
using this:
i \<le> j

goal (1 subgoal):
 1. closed i p \<Longrightarrow> closed j p
[PROOF STEP]
proof (induct p arbitrary: i j)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>i j. \<lbrakk>closed i FF; i \<le> j\<rbrakk> \<Longrightarrow> closed j FF
 2. \<And>i j. \<lbrakk>closed i TT; i \<le> j\<rbrakk> \<Longrightarrow> closed j TT
 3. \<And>x1 x2 i j. \<lbrakk>closed i (Pred x1 x2); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Pred x1 x2)
 4. \<And>p1 p2 i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p1; i \<le> j\<rbrakk> \<Longrightarrow> closed j p1; \<And>i j. \<lbrakk>closed i p2; i \<le> j\<rbrakk> \<Longrightarrow> closed j p2; closed i (And p1 p2); i \<le> j\<rbrakk> \<Longrightarrow> closed j (And p1 p2)
 5. \<And>p1 p2 i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p1; i \<le> j\<rbrakk> \<Longrightarrow> closed j p1; \<And>i j. \<lbrakk>closed i p2; i \<le> j\<rbrakk> \<Longrightarrow> closed j p2; closed i (Or p1 p2); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Or p1 p2)
 6. \<And>p1 p2 i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p1; i \<le> j\<rbrakk> \<Longrightarrow> closed j p1; \<And>i j. \<lbrakk>closed i p2; i \<le> j\<rbrakk> \<Longrightarrow> closed j p2; closed i (Impl p1 p2); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Impl p1 p2)
 7. \<And>p i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p; i \<le> j\<rbrakk> \<Longrightarrow> closed j p; closed i (Neg p); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Neg p)
 8. \<And>p i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p; i \<le> j\<rbrakk> \<Longrightarrow> closed j p; closed i (Forall p); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Forall p)
 9. \<And>p i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p; i \<le> j\<rbrakk> \<Longrightarrow> closed j p; closed i (Exists p); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Exists p)
[PROOF STEP]
case (Pred i l)
[PROOF STATE]
proof (state)
this:
closed i (Pred ia__ l)
i \<le> j

goal (9 subgoals):
 1. \<And>i j. \<lbrakk>closed i FF; i \<le> j\<rbrakk> \<Longrightarrow> closed j FF
 2. \<And>i j. \<lbrakk>closed i TT; i \<le> j\<rbrakk> \<Longrightarrow> closed j TT
 3. \<And>x1 x2 i j. \<lbrakk>closed i (Pred x1 x2); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Pred x1 x2)
 4. \<And>p1 p2 i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p1; i \<le> j\<rbrakk> \<Longrightarrow> closed j p1; \<And>i j. \<lbrakk>closed i p2; i \<le> j\<rbrakk> \<Longrightarrow> closed j p2; closed i (And p1 p2); i \<le> j\<rbrakk> \<Longrightarrow> closed j (And p1 p2)
 5. \<And>p1 p2 i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p1; i \<le> j\<rbrakk> \<Longrightarrow> closed j p1; \<And>i j. \<lbrakk>closed i p2; i \<le> j\<rbrakk> \<Longrightarrow> closed j p2; closed i (Or p1 p2); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Or p1 p2)
 6. \<And>p1 p2 i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p1; i \<le> j\<rbrakk> \<Longrightarrow> closed j p1; \<And>i j. \<lbrakk>closed i p2; i \<le> j\<rbrakk> \<Longrightarrow> closed j p2; closed i (Impl p1 p2); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Impl p1 p2)
 7. \<And>p i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p; i \<le> j\<rbrakk> \<Longrightarrow> closed j p; closed i (Neg p); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Neg p)
 8. \<And>p i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p; i \<le> j\<rbrakk> \<Longrightarrow> closed j p; closed i (Forall p); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Forall p)
 9. \<And>p i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p; i \<le> j\<rbrakk> \<Longrightarrow> closed j p; closed i (Exists p); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Exists p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closed i (Pred ia__ l)
i \<le> j
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
closed i (Pred ia__ l)
i \<le> j

goal (1 subgoal):
 1. closed j (Pred ia__ l)
[PROOF STEP]
using closedt_mono
[PROOF STATE]
proof (prove)
using this:
closed i (Pred ia__ l)
i \<le> j
\<lbrakk>?i \<le> ?j; closedt ?i ?t\<rbrakk> \<Longrightarrow> closedt ?j ?t
\<lbrakk>?i \<le> ?j; closedts ?i ?ts\<rbrakk> \<Longrightarrow> closedts ?j ?ts

goal (1 subgoal):
 1. closed j (Pred ia__ l)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
closed j (Pred ia__ l)

goal (8 subgoals):
 1. \<And>i j. \<lbrakk>closed i FF; i \<le> j\<rbrakk> \<Longrightarrow> closed j FF
 2. \<And>i j. \<lbrakk>closed i TT; i \<le> j\<rbrakk> \<Longrightarrow> closed j TT
 3. \<And>p1 p2 i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p1; i \<le> j\<rbrakk> \<Longrightarrow> closed j p1; \<And>i j. \<lbrakk>closed i p2; i \<le> j\<rbrakk> \<Longrightarrow> closed j p2; closed i (And p1 p2); i \<le> j\<rbrakk> \<Longrightarrow> closed j (And p1 p2)
 4. \<And>p1 p2 i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p1; i \<le> j\<rbrakk> \<Longrightarrow> closed j p1; \<And>i j. \<lbrakk>closed i p2; i \<le> j\<rbrakk> \<Longrightarrow> closed j p2; closed i (Or p1 p2); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Or p1 p2)
 5. \<And>p1 p2 i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p1; i \<le> j\<rbrakk> \<Longrightarrow> closed j p1; \<And>i j. \<lbrakk>closed i p2; i \<le> j\<rbrakk> \<Longrightarrow> closed j p2; closed i (Impl p1 p2); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Impl p1 p2)
 6. \<And>p i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p; i \<le> j\<rbrakk> \<Longrightarrow> closed j p; closed i (Neg p); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Neg p)
 7. \<And>p i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p; i \<le> j\<rbrakk> \<Longrightarrow> closed j p; closed i (Forall p); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Forall p)
 8. \<And>p i j. \<lbrakk>\<And>i j. \<lbrakk>closed i p; i \<le> j\<rbrakk> \<Longrightarrow> closed j p; closed i (Exists p); i \<le> j\<rbrakk> \<Longrightarrow> closed j (Exists p)
[PROOF STEP]
qed auto


[STATEMENT]
theorem lift_closed [simp]:
  \<open>closedt 0 (t::'a term) \<Longrightarrow> closedt 0 (liftt t)\<close>
  \<open>closedts 0 (ts::'a term list) \<Longrightarrow> closedts 0 (liftts ts)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (closedt 0 t \<Longrightarrow> closedt 0 (liftt t)) &&& (closedts 0 ts \<Longrightarrow> closedts 0 (liftts ts))
[PROOF STEP]
by (induct t and ts rule: closedt.induct closedts.induct) simp_all


[STATEMENT]
theorem subst_closedt [simp]:
  assumes u: \<open>closedt 0 u\<close>
  shows \<open>closedt (Suc i) t \<Longrightarrow> closedt i (t[u/i])\<close>
    and \<open>closedts (Suc i) ts \<Longrightarrow> closedts i (ts[u/i])\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (closedt (Suc i) t \<Longrightarrow> closedt i (t[u/i])) &&& (closedts (Suc i) ts \<Longrightarrow> closedts i (ts[u/i]))
[PROOF STEP]
using u closedt_mono(1)
[PROOF STATE]
proof (prove)
using this:
closedt 0 u
\<lbrakk>?i \<le> ?j; closedt ?i ?t\<rbrakk> \<Longrightarrow> closedt ?j ?t

goal (1 subgoal):
 1. (closedt (Suc i) t \<Longrightarrow> closedt i (t[u/i])) &&& (closedts (Suc i) ts \<Longrightarrow> closedts i (ts[u/i]))
[PROOF STEP]
by (induct t and ts rule: closedt.induct closedts.induct) auto


[STATEMENT]
theorem subst_closed [simp]:
  \<open>closedt 0 t \<Longrightarrow> closed (Suc i) p \<Longrightarrow> closed i (p[t/i])\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>closedt 0 t; closed (Suc i) p\<rbrakk> \<Longrightarrow> closed i (p[t/i])
[PROOF STEP]
by (induct p arbitrary: i t) simp_all


[STATEMENT]
theorem subst_size_form [simp]: \<open>size_form (subst p t i) = size_form p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FOL_Fitting.size_form (p[t/i]) = FOL_Fitting.size_form p
[PROOF STEP]
by (induct p arbitrary: i t) simp_all


[STATEMENT]
theorem psubstt_closed [simp]:
  \<open>closedt i (psubstt f t) = closedt i t\<close>
  \<open>closedts i (psubstts f ts) = closedts i ts\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closedt i (psubstt f t) = closedt i t &&& closedts i (psubstts f ts) = closedts i ts
[PROOF STEP]
by (induct t and ts rule: closedt.induct closedts.induct) simp_all


[STATEMENT]
theorem psubst_closed [simp]:
  \<open>closed i (psubst f p) = closed i p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed i (psubst f p) = closed i p
[PROOF STEP]
by (induct p arbitrary: i) simp_all


[STATEMENT]
theorem psubstt_subst [simp]:
  \<open>psubstt f (substt t u i) = substt (psubstt f t) (psubstt f u) i\<close>
  \<open>psubstts f (substts ts u i) = substts (psubstts f ts) (psubstt f u) i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubstt f (t[u/i]) = psubstt f t[psubstt f u/i] &&& psubstts f (ts[u/i]) = psubstts f ts[psubstt f u/i]
[PROOF STEP]
by (induct t and ts rule: psubstt.induct psubstts.induct) simp_all


[STATEMENT]
theorem psubstt_lift [simp]:
  \<open>psubstt f (liftt t) = liftt (psubstt f t)\<close>
  \<open>psubstts f (liftts ts) = liftts (psubstts f ts)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubstt f (liftt t) = liftt (psubstt f t) &&& psubstts f (liftts ts) = liftts (psubstts f ts)
[PROOF STEP]
by (induct t and ts rule: psubstt.induct psubstts.induct) simp_all


[STATEMENT]
theorem psubst_subst [simp]:
  \<open>psubst f (subst P t i) = subst (psubst f P) (psubstt f t) i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst f (P[t/i]) = psubst f P[psubstt f t/i]
[PROOF STEP]
by (induct P arbitrary: i t) simp_all


[STATEMENT]
theorem psubstt_upd [simp]:
  \<open>x \<notin> paramst (t::'a term) \<Longrightarrow> psubstt (f(x := y)) t = psubstt f t\<close>
  \<open>x \<notin> paramsts (ts::'a term list) \<Longrightarrow> psubstts (f(x := y)) ts = psubstts f ts\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<notin> paramst t \<Longrightarrow> psubstt (f(x := y)) t = psubstt f t) &&& (x \<notin> paramsts ts \<Longrightarrow> psubstts (f(x := y)) ts = psubstts f ts)
[PROOF STEP]
by (induct t and ts rule: psubstt.induct psubstts.induct) (auto split: sum.split)


[STATEMENT]
theorem psubst_upd [simp]: \<open>x \<notin> params P \<Longrightarrow> psubst (f(x := y)) P = psubst f P\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> params P \<Longrightarrow> psubst (f(x := y)) P = psubst f P
[PROOF STEP]
by (induct P) (simp_all del: fun_upd_apply)


[STATEMENT]
theorem psubstt_id:
  fixes t :: \<open>'a term\<close> and ts :: \<open>'a term list\<close>
  shows \<open>psubstt id t = t\<close> and \<open>psubstts (\<lambda>x. x) ts = ts\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubstt id t = t &&& psubstts (\<lambda>x. x) ts = ts
[PROOF STEP]
by (induct t and ts rule: psubstt.induct psubstts.induct) simp_all


[STATEMENT]
theorem psubstt_image [simp]:
  \<open>paramst (psubstt f t) = f ` paramst t\<close>
  \<open>paramsts (psubstts f ts) = f ` paramsts ts\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paramst (psubstt f t) = f ` paramst t &&& paramsts (psubstts f ts) = f ` paramsts ts
[PROOF STEP]
by (induct t and ts rule: paramst.induct paramsts.induct) (simp_all add: image_Un)


[STATEMENT]
theorem psubst_image [simp]: \<open>params (psubst f p) = f ` params p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. params (psubst f p) = f ` params p
[PROOF STEP]
by (induct p) (simp_all add: image_Un)


[STATEMENT]
lemma shift_gt [simp]: \<open>j < i \<Longrightarrow> (e\<langle>i:T\<rangle>) j = e j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < i \<Longrightarrow> (e\<langle>i:T\<rangle>) j = e j
[PROOF STEP]
by (simp add: shift_def)


[STATEMENT]
lemma shift_lt [simp]: \<open>i < j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = e (j - 1)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = e (j - 1)
[PROOF STEP]
by (simp add: shift_def)


[STATEMENT]
lemma shift_commute [simp]: \<open>e\<langle>i:U\<rangle>\<langle>0:T\<rangle> = e\<langle>0:T\<rangle>\<langle>Suc i:U\<rangle>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e\<langle>i:U\<rangle>\<langle>0:T\<rangle> = e\<langle>0:T\<rangle>\<langle>Suc i:U\<rangle>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (e\<langle>i:U\<rangle>\<langle>0:T\<rangle>) x = (e\<langle>0:T\<rangle>\<langle>Suc i:U\<rangle>) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (e\<langle>i:U\<rangle>\<langle>0:T\<rangle>) x = (e\<langle>0:T\<rangle>\<langle>Suc i:U\<rangle>) x
[PROOF STEP]
show \<open>(e\<langle>i:U\<rangle>\<langle>0:T\<rangle>) x = (e\<langle>0:T\<rangle>\<langle>Suc i:U\<rangle>) x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (e\<langle>i:U\<rangle>\<langle>0:T\<rangle>) x = (e\<langle>0:T\<rangle>\<langle>Suc i:U\<rangle>) x
[PROOF STEP]
by (cases x) (simp_all add: shift_def)
[PROOF STATE]
proof (state)
this:
(e\<langle>i:U\<rangle>\<langle>0:T\<rangle>) x = (e\<langle>0:T\<rangle>\<langle>Suc i:U\<rangle>) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem subst_lemma' [simp]:
  \<open>evalt e f (substt t u i) = evalt (e\<langle>i:evalt e f u\<rangle>) f t\<close>
  \<open>evalts e f (substts ts u i) = evalts (e\<langle>i:evalt e f u\<rangle>) f ts\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evalt e f (t[u/i]) = evalt (e\<langle>i:evalt e f u\<rangle>) f t &&& evalts e f (ts[u/i]) = evalts (e\<langle>i:evalt e f u\<rangle>) f ts
[PROOF STEP]
by (induct t and ts rule: substt.induct substts.induct) simp_all


[STATEMENT]
theorem lift_lemma [simp]:
  \<open>evalt (e\<langle>0:z\<rangle>) f (liftt t) = evalt e f t\<close>
  \<open>evalts (e\<langle>0:z\<rangle>) f (liftts ts) = evalts e f ts\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evalt (e\<langle>0:z\<rangle>) f (liftt t) = evalt e f t &&& evalts (e\<langle>0:z\<rangle>) f (liftts ts) = evalts e f ts
[PROOF STEP]
by (induct t and ts rule: liftt.induct liftts.induct) simp_all


[STATEMENT]
theorem subst_lemma [simp]:
  \<open>eval e f g (subst a t i) = eval (e\<langle>i:evalt e f t\<rangle>) f g a\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval e f g (a[t/i]) = eval (e\<langle>i:evalt e f t\<rangle>) f g a
[PROOF STEP]
by (induct a arbitrary: e i t) simp_all


[STATEMENT]
theorem upd_lemma' [simp]:
  \<open>n \<notin> paramst t \<Longrightarrow> evalt e (f(n := x)) t = evalt e f t\<close>
  \<open>n \<notin> paramsts ts \<Longrightarrow> evalts e (f(n := x)) ts = evalts e f ts\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n \<notin> paramst t \<Longrightarrow> evalt e (f(n := x)) t = evalt e f t) &&& (n \<notin> paramsts ts \<Longrightarrow> evalts e (f(n := x)) ts = evalts e f ts)
[PROOF STEP]
by (induct t and ts rule: paramst.induct paramsts.induct) auto


[STATEMENT]
theorem upd_lemma [simp]:
  \<open>n \<notin> params p \<Longrightarrow> eval e (f(n := x)) g p = eval e f g p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<notin> params p \<Longrightarrow> eval e (f(n := x)) g p = eval e f g p
[PROOF STEP]
by (induct p arbitrary: e) simp_all


[STATEMENT]
theorem list_upd_lemma [simp]: \<open>list_all (\<lambda>p. n \<notin> params p) G \<Longrightarrow>
  list_all (eval e (f(n := x)) g) G = list_all (eval e f g) G\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all (\<lambda>p. n \<notin> params p) G \<Longrightarrow> list_all (eval e (f(n := x)) g) G = list_all (eval e f g) G
[PROOF STEP]
by (induct G) simp_all


[STATEMENT]
theorem psubst_eval' [simp]:
  \<open>evalt e f (psubstt h t) = evalt e (\<lambda>p. f (h p)) t\<close>
  \<open>evalts e f (psubstts h ts) = evalts e (\<lambda>p. f (h p)) ts\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evalt e f (psubstt h t) = evalt e (\<lambda>p. f (h p)) t &&& evalts e f (psubstts h ts) = evalts e (\<lambda>p. f (h p)) ts
[PROOF STEP]
by (induct t and ts rule: psubstt.induct psubstts.induct) simp_all


[STATEMENT]
theorem psubst_eval:
  \<open>eval e f g (psubst h p) = eval e (\<lambda>p. f (h p)) g p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval e f g (psubst h p) = eval e (\<lambda>p. f (h p)) g p
[PROOF STEP]
by (induct p arbitrary: e) simp_all


[STATEMENT]
theorem ex_all_commute_eval:
  \<open>eval e f g (Impl (Exists (Forall (Pred p [Var 1, Var 0])))
    (Forall (Exists (Pred p [Var 0, Var 1]))))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval e f g (Impl (Exists (Forall (Pred p [Var 1, Var 0]))) (Forall (Exists (Pred p [Var 0, Var 1]))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>z. \<forall>za. g p [z, za]) \<longrightarrow> (\<forall>z. \<exists>za. g p [za, z])
[PROOF STEP]
txt \<open>
Simplification yields the following proof state:
@{subgoals [display]}
This is easily proved using intuitionistic logic:
\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>z. \<forall>za. g p [z, za]) \<longrightarrow> (\<forall>z. \<exists>za. g p [za, z])
[PROOF STEP]
by iprover


[STATEMENT]
theorem Class': \<open>Neg A # G \<turnstile> A \<Longrightarrow> G \<turnstile> A\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Neg A # G \<turnstile> A \<Longrightarrow> G \<turnstile> A
[PROOF STEP]
by (rule Class, rule NegE, rule Assum) (simp, iprover)


[STATEMENT]
theorem cut: \<open>G \<turnstile> A \<Longrightarrow> A # G \<turnstile> B \<Longrightarrow> G \<turnstile> B\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<turnstile> A; A # G \<turnstile> B\<rbrakk> \<Longrightarrow> G \<turnstile> B
[PROOF STEP]
by (rule ImplE, rule ImplI)


[STATEMENT]
theorem ForallE': \<open>G \<turnstile> Forall a \<Longrightarrow> subst a t 0 # G \<turnstile> B \<Longrightarrow> G \<turnstile> B\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<turnstile> Forall a; a[t/0] # G \<turnstile> B\<rbrakk> \<Longrightarrow> G \<turnstile> B
[PROOF STEP]
by (rule cut, rule ForallE)