[STATEMENT]
theorem Hahn_Banach:
  assumes E: "vectorspace E" and "subspace F E"
    and "seminorm E p" and "linearform F f"
  assumes fp: "\<forall>x \<in> F. f x \<le> p x"
  shows "\<exists>h. linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)"
    \<comment> \<open>Let \<open>E\<close> be a vector space, \<open>F\<close> a subspace of \<open>E\<close>, \<open>p\<close> a seminorm on \<open>E\<close>,\<close>
    \<comment> \<open>and \<open>f\<close> a linear form on \<open>F\<close> such that \<open>f\<close> is bounded by \<open>p\<close>,\<close>
    \<comment> \<open>then \<open>f\<close> can be extended to a linear form \<open>h\<close> on \<open>E\<close> in a norm-preserving way. \<^smallskip>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
interpret vectorspace E
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vectorspace E
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
interpret subspace F E
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Subspace.subspace F E
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
interpret seminorm E p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. seminorm E p
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
interpret linearform F f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linearform F f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
define M where "M = norm_pres_extensions E p F f"
[PROOF STATE]
proof (state)
this:
M = norm_pres_extensions E p F f

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
M = norm_pres_extensions E p F f
[PROOF STEP]
have M: "M = \<dots>"
[PROOF STATE]
proof (prove)
using this:
M = norm_pres_extensions E p F f

goal (1 subgoal):
 1. M = norm_pres_extensions E p F f
[PROOF STEP]
by (simp only:)
[PROOF STATE]
proof (state)
this:
M = norm_pres_extensions E p F f

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
from E
[PROOF STATE]
proof (chain)
picking this:
vectorspace E
[PROOF STEP]
have F: "vectorspace F"
[PROOF STATE]
proof (prove)
using this:
vectorspace E

goal (1 subgoal):
 1. vectorspace F
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
vectorspace F

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
note FE = \<open>F \<unlhd> E\<close>
[PROOF STATE]
proof (state)
this:
Subspace.subspace F E

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Subspace.subspace F E

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
assume cM: "c \<in> chains M" and ex: "\<exists>x. x \<in> c"
[PROOF STATE]
proof (state)
this:
c \<in> chains M
\<exists>x. x \<in> c

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
have "\<Union>c \<in> M"
      \<comment> \<open>Show that every non-empty chain \<open>c\<close> of \<open>M\<close> has an upper bound in \<open>M\<close>:\<close>
      \<comment> \<open>\<open>\<Union>c\<close> is greater than any element of the chain \<open>c\<close>, so it suffices to show \<open>\<Union>c \<in> M\<close>.\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> c \<in> M
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> c \<in> norm_pres_extensions E p F f
[PROOF STEP]
proof (rule norm_pres_extensionI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)
[PROOF STEP]
let ?H = "domain (\<Union>c)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)
[PROOF STEP]
let ?h = "funct (\<Union>c)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)
[PROOF STEP]
have a: "graph ?H ?h = \<Union>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph (domain (\<Union> c)) (funct (\<Union> c)) = \<Union> c
[PROOF STEP]
proof (rule graph_domain_funct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> \<Union> c; (x, z) \<in> \<Union> c\<rbrakk> \<Longrightarrow> z = y
[PROOF STEP]
fix x y z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> \<Union> c; (x, z) \<in> \<Union> c\<rbrakk> \<Longrightarrow> z = y
[PROOF STEP]
assume "(x, y) \<in> \<Union>c" and "(x, z) \<in> \<Union>c"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> \<Union> c
(x, z) \<in> \<Union> c

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> \<Union> c; (x, z) \<in> \<Union> c\<rbrakk> \<Longrightarrow> z = y
[PROOF STEP]
with M_def cM
[PROOF STATE]
proof (chain)
picking this:
M = norm_pres_extensions E p F f
c \<in> chains M
(x, y) \<in> \<Union> c
(x, z) \<in> \<Union> c
[PROOF STEP]
show "z = y"
[PROOF STATE]
proof (prove)
using this:
M = norm_pres_extensions E p F f
c \<in> chains M
(x, y) \<in> \<Union> c
(x, z) \<in> \<Union> c

goal (1 subgoal):
 1. z = y
[PROOF STEP]
by (rule sup_definite)
[PROOF STATE]
proof (state)
this:
z = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
graph (domain (\<Union> c)) (funct (\<Union> c)) = \<Union> c

goal (1 subgoal):
 1. \<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
graph (domain (\<Union> c)) (funct (\<Union> c)) = \<Union> c

goal (1 subgoal):
 1. \<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)
[PROOF STEP]
from M cM a
[PROOF STATE]
proof (chain)
picking this:
M = norm_pres_extensions E p F f
c \<in> chains M
graph (domain (\<Union> c)) (funct (\<Union> c)) = \<Union> c
[PROOF STEP]
have "linearform ?H ?h"
[PROOF STATE]
proof (prove)
using this:
M = norm_pres_extensions E p F f
c \<in> chains M
graph (domain (\<Union> c)) (funct (\<Union> c)) = \<Union> c

goal (1 subgoal):
 1. linearform (domain (\<Union> c)) (funct (\<Union> c))
[PROOF STEP]
by (rule sup_lf)
[PROOF STATE]
proof (state)
this:
linearform (domain (\<Union> c)) (funct (\<Union> c))

goal (1 subgoal):
 1. \<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
linearform (domain (\<Union> c)) (funct (\<Union> c))

goal (1 subgoal):
 1. \<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)
[PROOF STEP]
from a M cM ex FE E
[PROOF STATE]
proof (chain)
picking this:
graph (domain (\<Union> c)) (funct (\<Union> c)) = \<Union> c
M = norm_pres_extensions E p F f
c \<in> chains M
\<exists>x. x \<in> c
Subspace.subspace F E
vectorspace E
[PROOF STEP]
have "?H \<unlhd> E"
[PROOF STATE]
proof (prove)
using this:
graph (domain (\<Union> c)) (funct (\<Union> c)) = \<Union> c
M = norm_pres_extensions E p F f
c \<in> chains M
\<exists>x. x \<in> c
Subspace.subspace F E
vectorspace E

goal (1 subgoal):
 1. Subspace.subspace (domain (\<Union> c)) E
[PROOF STEP]
by (rule sup_subE)
[PROOF STATE]
proof (state)
this:
Subspace.subspace (domain (\<Union> c)) E

goal (1 subgoal):
 1. \<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Subspace.subspace (domain (\<Union> c)) E

goal (1 subgoal):
 1. \<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)
[PROOF STEP]
from a M cM ex FE
[PROOF STATE]
proof (chain)
picking this:
graph (domain (\<Union> c)) (funct (\<Union> c)) = \<Union> c
M = norm_pres_extensions E p F f
c \<in> chains M
\<exists>x. x \<in> c
Subspace.subspace F E
[PROOF STEP]
have "F \<unlhd> ?H"
[PROOF STATE]
proof (prove)
using this:
graph (domain (\<Union> c)) (funct (\<Union> c)) = \<Union> c
M = norm_pres_extensions E p F f
c \<in> chains M
\<exists>x. x \<in> c
Subspace.subspace F E

goal (1 subgoal):
 1. Subspace.subspace F (domain (\<Union> c))
[PROOF STEP]
by (rule sup_supF)
[PROOF STATE]
proof (state)
this:
Subspace.subspace F (domain (\<Union> c))

goal (1 subgoal):
 1. \<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Subspace.subspace F (domain (\<Union> c))

goal (1 subgoal):
 1. \<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)
[PROOF STEP]
from a M cM ex
[PROOF STATE]
proof (chain)
picking this:
graph (domain (\<Union> c)) (funct (\<Union> c)) = \<Union> c
M = norm_pres_extensions E p F f
c \<in> chains M
\<exists>x. x \<in> c
[PROOF STEP]
have "graph F f \<subseteq> graph ?H ?h"
[PROOF STATE]
proof (prove)
using this:
graph (domain (\<Union> c)) (funct (\<Union> c)) = \<Union> c
M = norm_pres_extensions E p F f
c \<in> chains M
\<exists>x. x \<in> c

goal (1 subgoal):
 1. graph F f \<subseteq> graph (domain (\<Union> c)) (funct (\<Union> c))
[PROOF STEP]
by (rule sup_ext)
[PROOF STATE]
proof (state)
this:
graph F f \<subseteq> graph (domain (\<Union> c)) (funct (\<Union> c))

goal (1 subgoal):
 1. \<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
graph F f \<subseteq> graph (domain (\<Union> c)) (funct (\<Union> c))

goal (1 subgoal):
 1. \<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)
[PROOF STEP]
from a M cM
[PROOF STATE]
proof (chain)
picking this:
graph (domain (\<Union> c)) (funct (\<Union> c)) = \<Union> c
M = norm_pres_extensions E p F f
c \<in> chains M
[PROOF STEP]
have "\<forall>x \<in> ?H. ?h x \<le> p x"
[PROOF STATE]
proof (prove)
using this:
graph (domain (\<Union> c)) (funct (\<Union> c)) = \<Union> c
M = norm_pres_extensions E p F f
c \<in> chains M

goal (1 subgoal):
 1. \<forall>x\<in>domain (\<Union> c). funct (\<Union> c) x \<le> p x
[PROOF STEP]
by (rule sup_norm_pres)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>domain (\<Union> c). funct (\<Union> c) x \<le> p x

goal (1 subgoal):
 1. \<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
graph (domain (\<Union> c)) (funct (\<Union> c)) = \<Union> c
linearform (domain (\<Union> c)) (funct (\<Union> c))
Subspace.subspace (domain (\<Union> c)) E
Subspace.subspace F (domain (\<Union> c))
graph F f \<subseteq> graph (domain (\<Union> c)) (funct (\<Union> c))
\<forall>x\<in>domain (\<Union> c). funct (\<Union> c) x \<le> p x
[PROOF STEP]
show "\<exists>H h. \<Union>c = graph H h
          \<and> linearform H h
          \<and> H \<unlhd> E
          \<and> F \<unlhd> H
          \<and> graph F f \<subseteq> graph H h
          \<and> (\<forall>x \<in> H. h x \<le> p x)"
[PROOF STATE]
proof (prove)
using this:
graph (domain (\<Union> c)) (funct (\<Union> c)) = \<Union> c
linearform (domain (\<Union> c)) (funct (\<Union> c))
Subspace.subspace (domain (\<Union> c)) E
Subspace.subspace F (domain (\<Union> c))
graph F f \<subseteq> graph (domain (\<Union> c)) (funct (\<Union> c))
\<forall>x\<in>domain (\<Union> c). funct (\<Union> c) x \<le> p x

goal (1 subgoal):
 1. \<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>H h. \<Union> c = graph H h \<and> linearform H h \<and> Subspace.subspace H E \<and> Subspace.subspace F H \<and> graph F f \<subseteq> graph H h \<and> (\<forall>x\<in>H. h x \<le> p x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union> c \<in> M

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?c2 \<in> chains M; \<exists>x. x \<in> ?c2\<rbrakk> \<Longrightarrow> \<Union> ?c2 \<in> M

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?c2 \<in> chains M; \<exists>x. x \<in> ?c2\<rbrakk> \<Longrightarrow> \<Union> ?c2 \<in> M
[PROOF STEP]
have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> x = g"
  \<comment> \<open>With Zorn's Lemma we can conclude that there is a maximal element in \<open>M\<close>. \<^smallskip>\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?c2 \<in> chains M; \<exists>x. x \<in> ?c2\<rbrakk> \<Longrightarrow> \<Union> ?c2 \<in> M

goal (1 subgoal):
 1. \<exists>g\<in>M. \<forall>x\<in>M. g \<subseteq> x \<longrightarrow> x = g
[PROOF STEP]
proof (rule Zorn's_Lemma)
      \<comment> \<open>We show that \<open>M\<close> is non-empty:\<close>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>c. \<lbrakk>c \<in> chains M; \<exists>x. x \<in> c\<rbrakk> \<Longrightarrow> c \<in> chains M
 2. \<And>c. \<lbrakk>c \<in> chains M; \<exists>x. x \<in> c\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> c
 3. ?a \<in> M
[PROOF STEP]
show "graph F f \<in> M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph F f \<in> M
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph F f \<in> norm_pres_extensions E p F f
[PROOF STEP]
proof (rule norm_pres_extensionI2)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. linearform F f
 2. Subspace.subspace F E
 3. Subspace.subspace F F
 4. graph F f \<subseteq> graph F f
 5. \<forall>x\<in>F. f x \<le> p x
[PROOF STEP]
show "linearform F f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linearform F f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
linearform F f

goal (4 subgoals):
 1. Subspace.subspace F E
 2. Subspace.subspace F F
 3. graph F f \<subseteq> graph F f
 4. \<forall>x\<in>F. f x \<le> p x
[PROOF STEP]
show "F \<unlhd> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Subspace.subspace F E
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Subspace.subspace F E

goal (3 subgoals):
 1. Subspace.subspace F F
 2. graph F f \<subseteq> graph F f
 3. \<forall>x\<in>F. f x \<le> p x
[PROOF STEP]
from F
[PROOF STATE]
proof (chain)
picking this:
vectorspace F
[PROOF STEP]
show "F \<unlhd> F"
[PROOF STATE]
proof (prove)
using this:
vectorspace F

goal (1 subgoal):
 1. Subspace.subspace F F
[PROOF STEP]
by (rule vectorspace.subspace_refl)
[PROOF STATE]
proof (state)
this:
Subspace.subspace F F

goal (2 subgoals):
 1. graph F f \<subseteq> graph F f
 2. \<forall>x\<in>F. f x \<le> p x
[PROOF STEP]
show "graph F f \<subseteq> graph F f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph F f \<subseteq> graph F f
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
graph F f \<subseteq> graph F f

goal (1 subgoal):
 1. \<forall>x\<in>F. f x \<le> p x
[PROOF STEP]
show "\<forall>x\<in>F. f x \<le> p x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>F. f x \<le> p x
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>F. f x \<le> p x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
graph F f \<in> M

goal (2 subgoals):
 1. \<And>c. \<lbrakk>c \<in> chains M; \<exists>x. x \<in> c\<rbrakk> \<Longrightarrow> c \<in> chains M
 2. \<And>c. \<lbrakk>c \<in> chains M; \<exists>x. x \<in> c\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> c
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>g\<in>M. \<forall>x\<in>M. g \<subseteq> x \<longrightarrow> x = g

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>g\<in>M. \<forall>x\<in>M. g \<subseteq> x \<longrightarrow> x = g
[PROOF STEP]
obtain g where gM: "g \<in> M" and gx: "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
[PROOF STATE]
proof (prove)
using this:
\<exists>g\<in>M. \<forall>x\<in>M. g \<subseteq> x \<longrightarrow> x = g

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> M; \<forall>x\<in>M. g \<subseteq> x \<longrightarrow> g = x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
g \<in> M
\<forall>x\<in>M. g \<subseteq> x \<longrightarrow> g = x

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
from gM
[PROOF STATE]
proof (chain)
picking this:
g \<in> M
[PROOF STEP]
obtain H h where
      g_rep: "g = graph H h"
    and linearform: "linearform H h"
    and HE: "H \<unlhd> E" and FH: "F \<unlhd> H"
    and graphs: "graph F f \<subseteq> graph H h"
    and hp: "\<forall>x \<in> H. h x \<le> p x"
[PROOF STATE]
proof (prove)
using this:
g \<in> M

goal (1 subgoal):
 1. (\<And>H h. \<lbrakk>g = graph H h; linearform H h; Subspace.subspace H E; Subspace.subspace F H; graph F f \<subseteq> graph H h; \<forall>x\<in>H. h x \<le> p x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
using this:
g \<in> norm_pres_extensions E p F f

goal (1 subgoal):
 1. (\<And>H h. \<lbrakk>g = graph H h; linearform H h; Subspace.subspace H E; Subspace.subspace F H; graph F f \<subseteq> graph H h; \<forall>x\<in>H. h x \<le> p x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
      \<comment> \<open>\<open>g\<close> is a norm-preserving extension of \<open>f\<close>, in other words:\<close>
      \<comment> \<open>\<open>g\<close> is the graph of some linear form \<open>h\<close> defined on a subspace \<open>H\<close> of \<open>E\<close>,\<close>
      \<comment> \<open>and \<open>h\<close> is an extension of \<open>f\<close> that is again bounded by \<open>p\<close>. \<^smallskip>\<close>
[PROOF STATE]
proof (state)
this:
g = graph H h
linearform H h
Subspace.subspace H E
Subspace.subspace F H
graph F f \<subseteq> graph H h
\<forall>x\<in>H. h x \<le> p x

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
from HE E
[PROOF STATE]
proof (chain)
picking this:
Subspace.subspace H E
vectorspace E
[PROOF STEP]
have H: "vectorspace H"
[PROOF STATE]
proof (prove)
using this:
Subspace.subspace H E
vectorspace E

goal (1 subgoal):
 1. vectorspace H
[PROOF STEP]
by (rule subspace.vectorspace)
[PROOF STATE]
proof (state)
this:
vectorspace H

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
have HE_eq: "H = E"
    \<comment> \<open>We show that \<open>h\<close> is defined on whole \<open>E\<close> by classical contradiction. \<^smallskip>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H = E
[PROOF STEP]
proof (rule classical)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<noteq> E \<Longrightarrow> H = E
[PROOF STEP]
assume neq: "H \<noteq> E"
      \<comment> \<open>Assume \<open>h\<close> is not defined on whole \<open>E\<close>. Then show that \<open>h\<close> can be extended\<close>
      \<comment> \<open>in a norm-preserving way to a function \<open>h'\<close> with the graph \<open>g'\<close>. \<^smallskip>\<close>
[PROOF STATE]
proof (state)
this:
H \<noteq> E

goal (1 subgoal):
 1. H \<noteq> E \<Longrightarrow> H = E
[PROOF STEP]
have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'
[PROOF STEP]
from HE
[PROOF STATE]
proof (chain)
picking this:
Subspace.subspace H E
[PROOF STEP]
have "H \<subseteq> E"
[PROOF STATE]
proof (prove)
using this:
Subspace.subspace H E

goal (1 subgoal):
 1. H \<subseteq> E
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
H \<subseteq> E

goal (1 subgoal):
 1. \<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'
[PROOF STEP]
with neq
[PROOF STATE]
proof (chain)
picking this:
H \<noteq> E
H \<subseteq> E
[PROOF STEP]
obtain x' where x'E: "x' \<in> E" and "x' \<notin> H"
[PROOF STATE]
proof (prove)
using this:
H \<noteq> E
H \<subseteq> E

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x' \<in> E; x' \<notin> H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x' \<in> E
x' \<notin> H

goal (1 subgoal):
 1. \<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'
[PROOF STEP]
obtain x': "x' \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x' \<noteq> (0::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x' \<noteq> (0::'a) \<Longrightarrow> thesis) \<Longrightarrow> x' \<noteq> (0::'a)
[PROOF STEP]
show "x' \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' \<noteq> (0::'a)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x' = (0::'a) \<Longrightarrow> False
[PROOF STEP]
assume "x' = 0"
[PROOF STATE]
proof (state)
this:
x' = (0::'a)

goal (1 subgoal):
 1. x' = (0::'a) \<Longrightarrow> False
[PROOF STEP]
with H
[PROOF STATE]
proof (chain)
picking this:
vectorspace H
x' = (0::'a)
[PROOF STEP]
have "x' \<in> H"
[PROOF STATE]
proof (prove)
using this:
vectorspace H
x' = (0::'a)

goal (1 subgoal):
 1. x' \<in> H
[PROOF STEP]
by (simp only: vectorspace.zero)
[PROOF STATE]
proof (state)
this:
x' \<in> H

goal (1 subgoal):
 1. x' = (0::'a) \<Longrightarrow> False
[PROOF STEP]
with \<open>x' \<notin> H\<close>
[PROOF STATE]
proof (chain)
picking this:
x' \<notin> H
x' \<in> H
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
x' \<notin> H
x' \<in> H

goal (1 subgoal):
 1. False
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x' \<noteq> (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x' \<noteq> (0::'a)

goal (1 subgoal):
 1. \<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'
[PROOF STEP]
define H' where "H' = H + lin x'"
        \<comment> \<open>Define \<open>H'\<close> as the direct sum of \<open>H\<close> and the linear closure of \<open>x'\<close>. \<^smallskip>\<close>
[PROOF STATE]
proof (state)
this:
H' = H + lin x'

goal (1 subgoal):
 1. \<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'
[PROOF STEP]
have HH': "H \<unlhd> H'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Subspace.subspace H H'
[PROOF STEP]
proof (unfold H'_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Subspace.subspace H (H + lin x')
[PROOF STEP]
from x'E
[PROOF STATE]
proof (chain)
picking this:
x' \<in> E
[PROOF STEP]
have "vectorspace (lin x')"
[PROOF STATE]
proof (prove)
using this:
x' \<in> E

goal (1 subgoal):
 1. vectorspace (lin x')
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
vectorspace (lin x')

goal (1 subgoal):
 1. Subspace.subspace H (H + lin x')
[PROOF STEP]
with H
[PROOF STATE]
proof (chain)
picking this:
vectorspace H
vectorspace (lin x')
[PROOF STEP]
show "H \<unlhd> H + lin x'"
[PROOF STATE]
proof (prove)
using this:
vectorspace H
vectorspace (lin x')

goal (1 subgoal):
 1. Subspace.subspace H (H + lin x')
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Subspace.subspace H (H + lin x')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Subspace.subspace H H'

goal (1 subgoal):
 1. \<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'
[PROOF STEP]
obtain xi where
        xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
          \<and> xi \<le> p (y + x') - h y"
        \<comment> \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequality; this will\<close>
        \<comment> \<open>be used to establish that \<open>h'\<close> is a norm-preserving extension of \<open>h\<close>.
           \label{ex-xi-use}\<^smallskip>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xi. \<forall>y\<in>H. - p (y + x') - h y \<le> xi \<and> xi \<le> p (y + x') - h y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>xi. \<forall>y\<in>H. - p (y + x') - h y \<le> xi \<and> xi \<le> p (y + x') - h y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from H
[PROOF STATE]
proof (chain)
picking this:
vectorspace H
[PROOF STEP]
have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y \<le> xi
            \<and> xi \<le> p (y + x') - h y"
[PROOF STATE]
proof (prove)
using this:
vectorspace H

goal (1 subgoal):
 1. \<exists>xi. \<forall>y\<in>H. - p (y + x') - h y \<le> xi \<and> xi \<le> p (y + x') - h y
[PROOF STEP]
proof (rule ex_xi)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
fix u v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
assume u: "u \<in> H" and v: "v \<in> H"
[PROOF STATE]
proof (state)
this:
u \<in> H
v \<in> H

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
with HE
[PROOF STATE]
proof (chain)
picking this:
Subspace.subspace H E
u \<in> H
v \<in> H
[PROOF STEP]
have uE: "u \<in> E" and vE: "v \<in> E"
[PROOF STATE]
proof (prove)
using this:
Subspace.subspace H E
u \<in> H
v \<in> H

goal (1 subgoal):
 1. u \<in> E &&& v \<in> E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> E
v \<in> E

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
from H u v linearform
[PROOF STATE]
proof (chain)
picking this:
vectorspace H
u \<in> H
v \<in> H
linearform H h
[PROOF STEP]
have "h v - h u = h (v - u)"
[PROOF STATE]
proof (prove)
using this:
vectorspace H
u \<in> H
v \<in> H
linearform H h

goal (1 subgoal):
 1. h v - h u = h (v - u)
[PROOF STEP]
by (simp add: linearform.diff)
[PROOF STATE]
proof (state)
this:
h v - h u = h (v - u)

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
h v - h u = h (v - u)

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
from hp and H u v
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>H. h x \<le> p x
vectorspace H
u \<in> H
v \<in> H
[PROOF STEP]
have "\<dots> \<le> p (v - u)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>H. h x \<le> p x
vectorspace H
u \<in> H
v \<in> H

goal (1 subgoal):
 1. h (v - u) \<le> p (v - u)
[PROOF STEP]
by (simp only: vectorspace.diff_closed)
[PROOF STATE]
proof (state)
this:
h (v - u) \<le> p (v - u)

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
h (v - u) \<le> p (v - u)

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
from x'E uE vE
[PROOF STATE]
proof (chain)
picking this:
x' \<in> E
u \<in> E
v \<in> E
[PROOF STEP]
have "v - u = x' + - x' + v + - u"
[PROOF STATE]
proof (prove)
using this:
x' \<in> E
u \<in> E
v \<in> E

goal (1 subgoal):
 1. v - u = x' + - x' + v + - u
[PROOF STEP]
by (simp add: diff_eq1)
[PROOF STATE]
proof (state)
this:
v - u = x' + - x' + v + - u

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
v - u = x' + - x' + v + - u

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
from x'E uE vE
[PROOF STATE]
proof (chain)
picking this:
x' \<in> E
u \<in> E
v \<in> E
[PROOF STEP]
have "\<dots> = v + x' + - (u + x')"
[PROOF STATE]
proof (prove)
using this:
x' \<in> E
u \<in> E
v \<in> E

goal (1 subgoal):
 1. x' + - x' + v + - u = v + x' + - (u + x')
[PROOF STEP]
by (simp add: add_ac)
[PROOF STATE]
proof (state)
this:
x' + - x' + v + - u = v + x' + - (u + x')

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x' + - x' + v + - u = v + x' + - (u + x')

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
from x'E uE vE
[PROOF STATE]
proof (chain)
picking this:
x' \<in> E
u \<in> E
v \<in> E
[PROOF STEP]
have "\<dots> = (v + x') - (u + x')"
[PROOF STATE]
proof (prove)
using this:
x' \<in> E
u \<in> E
v \<in> E

goal (1 subgoal):
 1. v + x' + - (u + x') = v + x' - (u + x')
[PROOF STEP]
by (simp add: diff_eq1)
[PROOF STATE]
proof (state)
this:
v + x' + - (u + x') = v + x' - (u + x')

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
v + x' + - (u + x') = v + x' - (u + x')

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
from x'E uE vE E
[PROOF STATE]
proof (chain)
picking this:
x' \<in> E
u \<in> E
v \<in> E
vectorspace E
[PROOF STEP]
have "p \<dots> \<le> p (v + x') + p (u + x')"
[PROOF STATE]
proof (prove)
using this:
x' \<in> E
u \<in> E
v \<in> E
vectorspace E

goal (1 subgoal):
 1. p (v + x' - (u + x')) \<le> p (v + x') + p (u + x')
[PROOF STEP]
by (simp add: diff_subadditive)
[PROOF STATE]
proof (state)
this:
p (v + x' - (u + x')) \<le> p (v + x') + p (u + x')

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
h v - h u \<le> p (v + x') + p (u + x')
[PROOF STEP]
have "h v - h u \<le> p (v + x') + p (u + x')"
[PROOF STATE]
proof (prove)
using this:
h v - h u \<le> p (v + x') + p (u + x')

goal (1 subgoal):
 1. h v - h u \<le> p (v + x') + p (u + x')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
h v - h u \<le> p (v + x') + p (u + x')

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> H; v \<in> H\<rbrakk> \<Longrightarrow> - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h v - h u \<le> p (v + x') + p (u + x')
[PROOF STEP]
show "- p (u + x') - h u \<le> p (v + x') - h v"
[PROOF STATE]
proof (prove)
using this:
h v - h u \<le> p (v + x') + p (u + x')

goal (1 subgoal):
 1. - p (u + x') - h u \<le> p (v + x') - h v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- p (u + x') - h u \<le> p (v + x') - h v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xi. \<forall>y\<in>H. - p (y + x') - h y \<le> xi \<and> xi \<le> p (y + x') - h y

goal (1 subgoal):
 1. (\<And>xi. \<forall>y\<in>H. - p (y + x') - h y \<le> xi \<and> xi \<le> p (y + x') - h y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>xi. \<forall>y\<in>H. - p (y + x') - h y \<le> xi \<and> xi \<le> p (y + x') - h y
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>xi. \<forall>y\<in>H. - p (y + x') - h y \<le> xi \<and> xi \<le> p (y + x') - h y

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (blast intro: that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>H. - p (y + x') - h y \<le> xi \<and> xi \<le> p (y + x') - h y

goal (1 subgoal):
 1. \<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'
[PROOF STEP]
define h' where "h' x = (let (y, a) =
          SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi)" for x
        \<comment> \<open>Define the extension \<open>h'\<close> of \<open>h\<close> to \<open>H'\<close> using \<open>\<xi>\<close>. \<^smallskip>\<close>
[PROOF STATE]
proof (state)
this:
h' ?x = (let (y, a) = SOME (y, a). ?x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi)

goal (1 subgoal):
 1. \<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'
[PROOF STEP]
have "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'"
        \<comment> \<open>\<open>h'\<close> is an extension of \<open>h\<close> \dots \<^smallskip>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. g \<subseteq> graph H' h'
 2. g \<noteq> graph H' h'
[PROOF STEP]
show "g \<subseteq> graph H' h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<subseteq> graph H' h'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g \<subseteq> graph H' h'
[PROOF STEP]
have "graph H h \<subseteq> graph H' h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph H h \<subseteq> graph H' h'
[PROOF STEP]
proof (rule graph_extI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> H \<Longrightarrow> h x = h' x
 2. H \<subseteq> H'
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> H \<Longrightarrow> h x = h' x
 2. H \<subseteq> H'
[PROOF STEP]
assume t: "t \<in> H"
[PROOF STATE]
proof (state)
this:
t \<in> H

goal (2 subgoals):
 1. \<And>x. x \<in> H \<Longrightarrow> h x = h' x
 2. H \<subseteq> H'
[PROOF STEP]
from E HE t
[PROOF STATE]
proof (chain)
picking this:
vectorspace E
Subspace.subspace H E
t \<in> H
[PROOF STEP]
have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
[PROOF STATE]
proof (prove)
using this:
vectorspace E
Subspace.subspace H E
t \<in> H

goal (1 subgoal):
 1. (SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)
[PROOF STEP]
using \<open>x' \<notin> H\<close> \<open>x' \<in> E\<close> \<open>x' \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
vectorspace E
Subspace.subspace H E
t \<in> H
x' \<notin> H
x' \<in> E
x' \<noteq> (0::'a)

goal (1 subgoal):
 1. (SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)
[PROOF STEP]
by (rule decomp_H'_H)
[PROOF STATE]
proof (state)
this:
(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)

goal (2 subgoals):
 1. \<And>x. x \<in> H \<Longrightarrow> h x = h' x
 2. H \<subseteq> H'
[PROOF STEP]
with h'_def
[PROOF STATE]
proof (chain)
picking this:
h' ?x = (let (y, a) = SOME (y, a). ?x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi)
(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)
[PROOF STEP]
show "h t = h' t"
[PROOF STATE]
proof (prove)
using this:
h' ?x = (let (y, a) = SOME (y, a). ?x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi)
(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)

goal (1 subgoal):
 1. h t = h' t
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
h t = h' t

goal (1 subgoal):
 1. H \<subseteq> H'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<subseteq> H'
[PROOF STEP]
from HH'
[PROOF STATE]
proof (chain)
picking this:
Subspace.subspace H H'
[PROOF STEP]
show "H \<subseteq> H'"
[PROOF STATE]
proof (prove)
using this:
Subspace.subspace H H'

goal (1 subgoal):
 1. H \<subseteq> H'
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
H \<subseteq> H'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
graph H h \<subseteq> graph H' h'

goal (1 subgoal):
 1. g \<subseteq> graph H' h'
[PROOF STEP]
with g_rep
[PROOF STATE]
proof (chain)
picking this:
g = graph H h
graph H h \<subseteq> graph H' h'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g = graph H h
graph H h \<subseteq> graph H' h'

goal (1 subgoal):
 1. g \<subseteq> graph H' h'
[PROOF STEP]
by (simp only:)
[PROOF STATE]
proof (state)
this:
g \<subseteq> graph H' h'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g \<subseteq> graph H' h'

goal (1 subgoal):
 1. g \<noteq> graph H' h'
[PROOF STEP]
show "g \<noteq> graph H' h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<noteq> graph H' h'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g \<noteq> graph H' h'
[PROOF STEP]
have "graph H h \<noteq> graph H' h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph H h \<noteq> graph H' h'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. graph H h = graph H' h' \<Longrightarrow> False
[PROOF STEP]
assume eq: "graph H h = graph H' h'"
[PROOF STATE]
proof (state)
this:
graph H h = graph H' h'

goal (1 subgoal):
 1. graph H h = graph H' h' \<Longrightarrow> False
[PROOF STEP]
have "x' \<in> H'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' \<in> H'
[PROOF STEP]
unfolding H'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' \<in> H + lin x'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?u \<in> H
 2. ?v \<in> lin x'
 3. x' = ?u + ?v
[PROOF STEP]
from H
[PROOF STATE]
proof (chain)
picking this:
vectorspace H
[PROOF STEP]
show "0 \<in> H"
[PROOF STATE]
proof (prove)
using this:
vectorspace H

goal (1 subgoal):
 1. (0::'a) \<in> H
[PROOF STEP]
by (rule vectorspace.zero)
[PROOF STATE]
proof (state)
this:
(0::'a) \<in> H

goal (2 subgoals):
 1. ?v \<in> lin x'
 2. x' = (0::'a) + ?v
[PROOF STEP]
from x'E
[PROOF STATE]
proof (chain)
picking this:
x' \<in> E
[PROOF STEP]
show "x' \<in> lin x'"
[PROOF STATE]
proof (prove)
using this:
x' \<in> E

goal (1 subgoal):
 1. x' \<in> lin x'
[PROOF STEP]
by (rule x_lin_x)
[PROOF STATE]
proof (state)
this:
x' \<in> lin x'

goal (1 subgoal):
 1. x' = (0::'a) + x'
[PROOF STEP]
from x'E
[PROOF STATE]
proof (chain)
picking this:
x' \<in> E
[PROOF STEP]
show "x' = 0 + x'"
[PROOF STATE]
proof (prove)
using this:
x' \<in> E

goal (1 subgoal):
 1. x' = (0::'a) + x'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x' = (0::'a) + x'

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

goal (1 subgoal):
 1. graph H h = graph H' h' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x' \<in> H'
[PROOF STEP]
have "(x', h' x') \<in> graph H' h'"
[PROOF STATE]
proof (prove)
using this:
x' \<in> H'

goal (1 subgoal):
 1. (x', h' x') \<in> graph H' h'
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(x', h' x') \<in> graph H' h'

goal (1 subgoal):
 1. graph H h = graph H' h' \<Longrightarrow> False
[PROOF STEP]
with eq
[PROOF STATE]
proof (chain)
picking this:
graph H h = graph H' h'
(x', h' x') \<in> graph H' h'
[PROOF STEP]
have "(x', h' x') \<in> graph H h"
[PROOF STATE]
proof (prove)
using this:
graph H h = graph H' h'
(x', h' x') \<in> graph H' h'

goal (1 subgoal):
 1. (x', h' x') \<in> graph H h
[PROOF STEP]
by (simp only:)
[PROOF STATE]
proof (state)
this:
(x', h' x') \<in> graph H h

goal (1 subgoal):
 1. graph H h = graph H' h' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x', h' x') \<in> graph H h
[PROOF STEP]
have "x' \<in> H"
[PROOF STATE]
proof (prove)
using this:
(x', h' x') \<in> graph H h

goal (1 subgoal):
 1. x' \<in> H
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x' \<in> H

goal (1 subgoal):
 1. graph H h = graph H' h' \<Longrightarrow> False
[PROOF STEP]
with \<open>x' \<notin> H\<close>
[PROOF STATE]
proof (chain)
picking this:
x' \<notin> H
x' \<in> H
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
x' \<notin> H
x' \<in> H

goal (1 subgoal):
 1. False
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
graph H h \<noteq> graph H' h'

goal (1 subgoal):
 1. g \<noteq> graph H' h'
[PROOF STEP]
with g_rep
[PROOF STATE]
proof (chain)
picking this:
g = graph H h
graph H h \<noteq> graph H' h'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g = graph H h
graph H h \<noteq> graph H' h'

goal (1 subgoal):
 1. g \<noteq> graph H' h'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g \<noteq> graph H' h'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g \<noteq> graph H' h'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'

goal (1 subgoal):
 1. \<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'

goal (1 subgoal):
 1. \<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'
[PROOF STEP]
have "graph H' h' \<in> M"
        \<comment> \<open>and \<open>h'\<close> is norm-preserving. \<^smallskip>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph H' h' \<in> M
[PROOF STEP]
proof (unfold M_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. graph H' h' \<in> norm_pres_extensions E p F f
[PROOF STEP]
show "graph H' h' \<in> norm_pres_extensions E p F f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph H' h' \<in> norm_pres_extensions E p F f
[PROOF STEP]
proof (rule norm_pres_extensionI2)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. linearform H' h'
 2. Subspace.subspace H' E
 3. Subspace.subspace F H'
 4. graph F f \<subseteq> graph H' h'
 5. \<forall>x\<in>H'. h' x \<le> p x
[PROOF STEP]
show "linearform H' h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linearform H' h'
[PROOF STEP]
using h'_def H'_def HE linearform \<open>x' \<notin> H\<close> \<open>x' \<in> E\<close> \<open>x' \<noteq> 0\<close> E
[PROOF STATE]
proof (prove)
using this:
h' ?x = (let (y, a) = SOME (y, a). ?x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi)
H' = H + lin x'
Subspace.subspace H E
linearform H h
x' \<notin> H
x' \<in> E
x' \<noteq> (0::'a)
vectorspace E

goal (1 subgoal):
 1. linearform H' h'
[PROOF STEP]
by (rule h'_lf)
[PROOF STATE]
proof (state)
this:
linearform H' h'

goal (4 subgoals):
 1. Subspace.subspace H' E
 2. Subspace.subspace F H'
 3. graph F f \<subseteq> graph H' h'
 4. \<forall>x\<in>H'. h' x \<le> p x
[PROOF STEP]
show "H' \<unlhd> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Subspace.subspace H' E
[PROOF STEP]
unfolding H'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Subspace.subspace (H + lin x') E
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Subspace.subspace H E
 2. vectorspace E
 3. Subspace.subspace (lin x') E
[PROOF STEP]
show "H \<unlhd> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Subspace.subspace H E
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Subspace.subspace H E

goal (2 subgoals):
 1. vectorspace E
 2. Subspace.subspace (lin x') E
[PROOF STEP]
show "vectorspace E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vectorspace E
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
vectorspace E

goal (1 subgoal):
 1. Subspace.subspace (lin x') E
[PROOF STEP]
from x'E
[PROOF STATE]
proof (chain)
picking this:
x' \<in> E
[PROOF STEP]
show "lin x' \<unlhd> E"
[PROOF STATE]
proof (prove)
using this:
x' \<in> E

goal (1 subgoal):
 1. Subspace.subspace (lin x') E
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Subspace.subspace (lin x') E

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Subspace.subspace H' E

goal (3 subgoals):
 1. Subspace.subspace F H'
 2. graph F f \<subseteq> graph H' h'
 3. \<forall>x\<in>H'. h' x \<le> p x
[PROOF STEP]
from H \<open>F \<unlhd> H\<close> HH'
[PROOF STATE]
proof (chain)
picking this:
vectorspace H
Subspace.subspace F H
Subspace.subspace H H'
[PROOF STEP]
show FH': "F \<unlhd> H'"
[PROOF STATE]
proof (prove)
using this:
vectorspace H
Subspace.subspace F H
Subspace.subspace H H'

goal (1 subgoal):
 1. Subspace.subspace F H'
[PROOF STEP]
by (rule vectorspace.subspace_trans)
[PROOF STATE]
proof (state)
this:
Subspace.subspace F H'

goal (2 subgoals):
 1. graph F f \<subseteq> graph H' h'
 2. \<forall>x\<in>H'. h' x \<le> p x
[PROOF STEP]
show "graph F f \<subseteq> graph H' h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph F f \<subseteq> graph H' h'
[PROOF STEP]
proof (rule graph_extI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> F \<Longrightarrow> f x = h' x
 2. F \<subseteq> H'
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> F \<Longrightarrow> f x = h' x
 2. F \<subseteq> H'
[PROOF STEP]
assume x: "x \<in> F"
[PROOF STATE]
proof (state)
this:
x \<in> F

goal (2 subgoals):
 1. \<And>x. x \<in> F \<Longrightarrow> f x = h' x
 2. F \<subseteq> H'
[PROOF STEP]
with graphs
[PROOF STATE]
proof (chain)
picking this:
graph F f \<subseteq> graph H h
x \<in> F
[PROOF STEP]
have "f x = h x"
[PROOF STATE]
proof (prove)
using this:
graph F f \<subseteq> graph H h
x \<in> F

goal (1 subgoal):
 1. f x = h x
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
f x = h x

goal (2 subgoals):
 1. \<And>x. x \<in> F \<Longrightarrow> f x = h' x
 2. F \<subseteq> H'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f x = h x

goal (2 subgoals):
 1. \<And>x. x \<in> F \<Longrightarrow> f x = h' x
 2. F \<subseteq> H'
[PROOF STEP]
have "\<dots> = h x + 0 * xi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h x = h x + 0 * xi
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h x = h x + 0 * xi

goal (2 subgoals):
 1. \<And>x. x \<in> F \<Longrightarrow> f x = h' x
 2. F \<subseteq> H'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
h x = h x + 0 * xi

goal (2 subgoals):
 1. \<And>x. x \<in> F \<Longrightarrow> f x = h' x
 2. F \<subseteq> H'
[PROOF STEP]
have "\<dots> = (let (y, a) = (x, 0) in h y + a * xi)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h x + 0 * xi = (let (y, a) = (x, 0) in h y + a * xi)
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
h x + 0 * xi = (let (y, a) = (x, 0) in h y + a * xi)

goal (2 subgoals):
 1. \<And>x. x \<in> F \<Longrightarrow> f x = h' x
 2. F \<subseteq> H'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
h x + 0 * xi = (let (y, a) = (x, 0) in h y + a * xi)

goal (2 subgoals):
 1. \<And>x. x \<in> F \<Longrightarrow> f x = h' x
 2. F \<subseteq> H'
[PROOF STEP]
have "(x, 0) =
                (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, 0) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)
[PROOF STEP]
using E HE
[PROOF STATE]
proof (prove)
using this:
vectorspace E
Subspace.subspace H E

goal (1 subgoal):
 1. (x, 0) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)
[PROOF STEP]
proof (rule decomp_H'_H [symmetric])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. x \<in> H
 2. x' \<notin> H
 3. x' \<in> E
 4. x' \<noteq> (0::'a)
[PROOF STEP]
from FH x
[PROOF STATE]
proof (chain)
picking this:
Subspace.subspace F H
x \<in> F
[PROOF STEP]
show "x \<in> H"
[PROOF STATE]
proof (prove)
using this:
Subspace.subspace F H
x \<in> F

goal (1 subgoal):
 1. x \<in> H
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x \<in> H

goal (3 subgoals):
 1. x' \<notin> H
 2. x' \<in> E
 3. x' \<noteq> (0::'a)
[PROOF STEP]
from x'
[PROOF STATE]
proof (chain)
picking this:
x' \<noteq> (0::'a)
[PROOF STEP]
show "x' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
x' \<noteq> (0::'a)

goal (1 subgoal):
 1. x' \<noteq> (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x' \<noteq> (0::'a)

goal (2 subgoals):
 1. x' \<notin> H
 2. x' \<in> E
[PROOF STEP]
show "x' \<notin> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' \<notin> H
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
x' \<notin> H

goal (1 subgoal):
 1. x' \<in> E
[PROOF STEP]
show "x' \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' \<in> E
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
x' \<in> E

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x, 0) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)

goal (2 subgoals):
 1. \<And>x. x \<in> F \<Longrightarrow> f x = h' x
 2. F \<subseteq> H'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x, 0) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)

goal (2 subgoals):
 1. \<And>x. x \<in> F \<Longrightarrow> f x = h' x
 2. F \<subseteq> H'
[PROOF STEP]
have
              "(let (y, a) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)
              in h y + a * xi) = h' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let (y, a) = SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi) = h' x
[PROOF STEP]
by (simp only: h'_def)
[PROOF STATE]
proof (state)
this:
(let (y, a) = SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi) = h' x

goal (2 subgoals):
 1. \<And>x. x \<in> F \<Longrightarrow> f x = h' x
 2. F \<subseteq> H'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f x = h' x
[PROOF STEP]
show "f x = h' x"
[PROOF STATE]
proof (prove)
using this:
f x = h' x

goal (1 subgoal):
 1. f x = h' x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f x = h' x

goal (1 subgoal):
 1. F \<subseteq> H'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. F \<subseteq> H'
[PROOF STEP]
from FH'
[PROOF STATE]
proof (chain)
picking this:
Subspace.subspace F H'
[PROOF STEP]
show "F \<subseteq> H'"
[PROOF STATE]
proof (prove)
using this:
Subspace.subspace F H'

goal (1 subgoal):
 1. F \<subseteq> H'
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
F \<subseteq> H'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
graph F f \<subseteq> graph H' h'

goal (1 subgoal):
 1. \<forall>x\<in>H'. h' x \<le> p x
[PROOF STEP]
show "\<forall>x \<in> H'. h' x \<le> p x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>H'. h' x \<le> p x
[PROOF STEP]
using h'_def H'_def \<open>x' \<notin> H\<close> \<open>x' \<in> E\<close> \<open>x' \<noteq> 0\<close> E HE
              \<open>seminorm E p\<close> linearform and hp xi
[PROOF STATE]
proof (prove)
using this:
h' ?x = (let (y, a) = SOME (y, a). ?x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi)
H' = H + lin x'
x' \<notin> H
x' \<in> E
x' \<noteq> (0::'a)
vectorspace E
Subspace.subspace H E
seminorm E p
linearform H h
\<forall>x\<in>H. h x \<le> p x
\<forall>y\<in>H. - p (y + x') - h y \<le> xi \<and> xi \<le> p (y + x') - h y

goal (1 subgoal):
 1. \<forall>x\<in>H'. h' x \<le> p x
[PROOF STEP]
by (rule h'_norm_pres)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>H'. h' x \<le> p x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
graph H' h' \<in> norm_pres_extensions E p F f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
graph H' h' \<in> M

goal (1 subgoal):
 1. \<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'
graph H' h' \<in> M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'
graph H' h' \<in> M

goal (1 subgoal):
 1. \<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'

goal (1 subgoal):
 1. H \<noteq> E \<Longrightarrow> H = E
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'
[PROOF STEP]
have "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>g'\<in>M. g \<subseteq> g' \<and> g \<noteq> g'

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>M. g \<subseteq> x \<longrightarrow> g = x)
[PROOF STEP]
by simp
      \<comment> \<open>So the graph \<open>g\<close> of \<open>h\<close> cannot be maximal. Contradiction! \<^smallskip>\<close>
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>x\<in>M. g \<subseteq> x \<longrightarrow> g = x)

goal (1 subgoal):
 1. H \<noteq> E \<Longrightarrow> H = E
[PROOF STEP]
with gx
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>M. g \<subseteq> x \<longrightarrow> g = x
\<not> (\<forall>x\<in>M. g \<subseteq> x \<longrightarrow> g = x)
[PROOF STEP]
show "H = E"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>M. g \<subseteq> x \<longrightarrow> g = x
\<not> (\<forall>x\<in>M. g \<subseteq> x \<longrightarrow> g = x)

goal (1 subgoal):
 1. H = E
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
H = E

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
H = E

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
from HE_eq and linearform
[PROOF STATE]
proof (chain)
picking this:
H = E
linearform H h
[PROOF STEP]
have "linearform E h"
[PROOF STATE]
proof (prove)
using this:
H = E
linearform H h

goal (1 subgoal):
 1. linearform E h
[PROOF STEP]
by (simp only:)
[PROOF STATE]
proof (state)
this:
linearform E h

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
linearform E h

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
have "\<forall>x \<in> F. h x = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>F. h x = f x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> F \<Longrightarrow> h x = f x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> F \<Longrightarrow> h x = f x
[PROOF STEP]
assume "x \<in> F"
[PROOF STATE]
proof (state)
this:
x \<in> F

goal (1 subgoal):
 1. \<And>x. x \<in> F \<Longrightarrow> h x = f x
[PROOF STEP]
with graphs
[PROOF STATE]
proof (chain)
picking this:
graph F f \<subseteq> graph H h
x \<in> F
[PROOF STEP]
have "f x = h x"
[PROOF STATE]
proof (prove)
using this:
graph F f \<subseteq> graph H h
x \<in> F

goal (1 subgoal):
 1. f x = h x
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
f x = h x

goal (1 subgoal):
 1. \<And>x. x \<in> F \<Longrightarrow> h x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f x = h x
[PROOF STEP]
show "h x = f x"
[PROOF STATE]
proof (prove)
using this:
f x = h x

goal (1 subgoal):
 1. h x = f x
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
h x = f x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>F. h x = f x

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>F. h x = f x

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
from HE_eq and hp
[PROOF STATE]
proof (chain)
picking this:
H = E
\<forall>x\<in>H. h x \<le> p x
[PROOF STEP]
have "\<forall>x \<in> E. h x \<le> p x"
[PROOF STATE]
proof (prove)
using this:
H = E
\<forall>x\<in>H. h x \<le> p x

goal (1 subgoal):
 1. \<forall>x\<in>E. h x \<le> p x
[PROOF STEP]
by (simp only:)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>E. h x \<le> p x

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
linearform E h
\<forall>x\<in>F. h x = f x
\<forall>x\<in>E. h x \<le> p x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
linearform E h
\<forall>x\<in>F. h x = f x
\<forall>x\<in>E. h x \<le> p x

goal (1 subgoal):
 1. \<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>h. linearform E h \<and> (\<forall>x\<in>F. h x = f x) \<and> (\<forall>x\<in>E. h x \<le> p x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Pi_empty [simp]: "Pi {} B = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pi {} B = UNIV
[PROOF STEP]
by (simp add: Pi_def)


[STATEMENT]
lemma lookup_delete[simp]: "lookup (delete k m) k = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (delete k m) k = None
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma lookup_default_neq: "x \<noteq> y \<Longrightarrow> lookup (default x d m) y = lookup m y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> lookup (Mapping.default x d m) y = lookup m y
[PROOF STEP]
unfolding lookup_default_def default_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> lookup (if x \<in> keys m then m else update x d m) y = lookup m y
[PROOF STEP]
by transfer (auto split: option.splits)


[STATEMENT]
lemma (in prob_space) real_distribution_distr [intro, simp]:
  "random_variable borel X \<Longrightarrow> real_distribution (distr M borel X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. random_variable borel X \<Longrightarrow> real_distribution (distr M borel X)
[PROOF STEP]
unfolding real_distribution_def real_distribution_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. random_variable borel X \<Longrightarrow> prob_space (distr M borel X) \<and> sets (distr M borel X) = sets borel
[PROOF STEP]
by (auto intro!: prob_space_distr)


[STATEMENT]
lemma floorlog_eq_zero_iff:
  "floorlog b x = 0 \<longleftrightarrow> b \<le> 1 \<or> x \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (floorlog b x = 0) = (b \<le> 1 \<or> x \<le> 0)
[PROOF STEP]
by (auto simp: floorlog_def)


[STATEMENT]
lemma simple_function_comp:
  assumes T: "T \<in> measurable M M'"
    and f: "simple_function M' f"
  shows "simple_function M (\<lambda>x. f (T x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_function M (\<lambda>x. f (T x))
[PROOF STEP]
proof (intro simple_function_def[THEN iffD2] conjI ballI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite ((\<lambda>x. f (T x)) ` space M)
 2. \<And>x. x \<in> (\<lambda>x. f (T x)) ` space M \<Longrightarrow> (\<lambda>x. f (T x)) -` {x} \<inter> space M \<in> sets M
[PROOF STEP]
have "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'
[PROOF STEP]
using T
[PROOF STATE]
proof (prove)
using this:
T \<in> M \<rightarrow>\<^sub>M M'

goal (1 subgoal):
 1. (\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'
[PROOF STEP]
unfolding measurable_def
[PROOF STATE]
proof (prove)
using this:
T \<in> {f \<in> space M \<rightarrow> space M'. \<forall>y\<in>sets M'. f -` y \<inter> space M \<in> sets M}

goal (1 subgoal):
 1. (\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'

goal (2 subgoals):
 1. finite ((\<lambda>x. f (T x)) ` space M)
 2. \<And>x. x \<in> (\<lambda>x. f (T x)) ` space M \<Longrightarrow> (\<lambda>x. f (T x)) -` {x} \<inter> space M \<in> sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'
[PROOF STEP]
show "finite ((\<lambda>x. f (T x)) ` space M)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'

goal (1 subgoal):
 1. finite ((\<lambda>x. f (T x)) ` space M)
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'
simple_function M' f

goal (1 subgoal):
 1. finite ((\<lambda>x. f (T x)) ` space M)
[PROOF STEP]
unfolding simple_function_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'
finite (f ` space M') \<and> (\<forall>x\<in>f ` space M'. f -` {x} \<inter> space M' \<in> sets M')

goal (1 subgoal):
 1. finite ((\<lambda>x. f (T x)) ` space M)
[PROOF STEP]
by (auto intro: finite_subset)
[PROOF STATE]
proof (state)
this:
finite ((\<lambda>x. f (T x)) ` space M)

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. f (T x)) ` space M \<Longrightarrow> (\<lambda>x. f (T x)) -` {x} \<inter> space M \<in> sets M
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. f (T x)) ` space M \<Longrightarrow> (\<lambda>x. f (T x)) -` {x} \<inter> space M \<in> sets M
[PROOF STEP]
assume i: "i \<in> (\<lambda>x. f (T x)) ` space M"
[PROOF STATE]
proof (state)
this:
i \<in> (\<lambda>x. f (T x)) ` space M

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. f (T x)) ` space M \<Longrightarrow> (\<lambda>x. f (T x)) -` {x} \<inter> space M \<in> sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> (\<lambda>x. f (T x)) ` space M
[PROOF STEP]
have "i \<in> f ` space M'"
[PROOF STATE]
proof (prove)
using this:
i \<in> (\<lambda>x. f (T x)) ` space M

goal (1 subgoal):
 1. i \<in> f ` space M'
[PROOF STEP]
using T
[PROOF STATE]
proof (prove)
using this:
i \<in> (\<lambda>x. f (T x)) ` space M
T \<in> M \<rightarrow>\<^sub>M M'

goal (1 subgoal):
 1. i \<in> f ` space M'
[PROOF STEP]
unfolding measurable_def
[PROOF STATE]
proof (prove)
using this:
i \<in> (\<lambda>x. f (T x)) ` space M
T \<in> {f \<in> space M \<rightarrow> space M'. \<forall>y\<in>sets M'. f -` y \<inter> space M \<in> sets M}

goal (1 subgoal):
 1. i \<in> f ` space M'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<in> f ` space M'

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. f (T x)) ` space M \<Longrightarrow> (\<lambda>x. f (T x)) -` {x} \<inter> space M \<in> sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> f ` space M'
[PROOF STEP]
have "f -` {i} \<inter> space M' \<in> sets M'"
[PROOF STATE]
proof (prove)
using this:
i \<in> f ` space M'

goal (1 subgoal):
 1. f -` {i} \<inter> space M' \<in> sets M'
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
i \<in> f ` space M'
simple_function M' f

goal (1 subgoal):
 1. f -` {i} \<inter> space M' \<in> sets M'
[PROOF STEP]
unfolding simple_function_def
[PROOF STATE]
proof (prove)
using this:
i \<in> f ` space M'
finite (f ` space M') \<and> (\<forall>x\<in>f ` space M'. f -` {x} \<inter> space M' \<in> sets M')

goal (1 subgoal):
 1. f -` {i} \<inter> space M' \<in> sets M'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f -` {i} \<inter> space M' \<in> sets M'

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. f (T x)) ` space M \<Longrightarrow> (\<lambda>x. f (T x)) -` {x} \<inter> space M \<in> sets M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f -` {i} \<inter> space M' \<in> sets M'
[PROOF STEP]
have "T -` (f -` {i} \<inter> space M') \<inter> space M \<in> sets M"
[PROOF STATE]
proof (prove)
using this:
f -` {i} \<inter> space M' \<in> sets M'

goal (1 subgoal):
 1. T -` (f -` {i} \<inter> space M') \<inter> space M \<in> sets M
[PROOF STEP]
using T
[PROOF STATE]
proof (prove)
using this:
f -` {i} \<inter> space M' \<in> sets M'
T \<in> M \<rightarrow>\<^sub>M M'

goal (1 subgoal):
 1. T -` (f -` {i} \<inter> space M') \<inter> space M \<in> sets M
[PROOF STEP]
unfolding measurable_def
[PROOF STATE]
proof (prove)
using this:
f -` {i} \<inter> space M' \<in> sets M'
T \<in> {f \<in> space M \<rightarrow> space M'. \<forall>y\<in>sets M'. f -` y \<inter> space M \<in> sets M}

goal (1 subgoal):
 1. T -` (f -` {i} \<inter> space M') \<inter> space M \<in> sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T -` (f -` {i} \<inter> space M') \<inter> space M \<in> sets M

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. f (T x)) ` space M \<Longrightarrow> (\<lambda>x. f (T x)) -` {x} \<inter> space M \<in> sets M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T -` (f -` {i} \<inter> space M') \<inter> space M \<in> sets M

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. f (T x)) ` space M \<Longrightarrow> (\<lambda>x. f (T x)) -` {x} \<inter> space M \<in> sets M
[PROOF STEP]
have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M
[PROOF STEP]
using T
[PROOF STATE]
proof (prove)
using this:
T \<in> M \<rightarrow>\<^sub>M M'

goal (1 subgoal):
 1. T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M
[PROOF STEP]
unfolding measurable_def
[PROOF STATE]
proof (prove)
using this:
T \<in> {f \<in> space M \<rightarrow> space M'. \<forall>y\<in>sets M'. f -` y \<inter> space M \<in> sets M}

goal (1 subgoal):
 1. T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. f (T x)) ` space M \<Longrightarrow> (\<lambda>x. f (T x)) -` {x} \<inter> space M \<in> sets M
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M
[PROOF STEP]
show "(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M

goal (1 subgoal):
 1. (\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma C_prod_eq_D_times_E: "prod id E * prod id D = prod id C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod id E * prod id D = prod id C
[PROOF STEP]
by (metis C_eq D_E_disj finite_D finite_E inf_commute prod.union_disjoint sup_commute)


[STATEMENT]
lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. List h p as \<Longrightarrow> \<exists>!as. List h p as
[PROOF STEP]
by(blast intro:List_unique)


[STATEMENT]
lemma fm_image_measurable_finite:
  assumes "space M = UNIV"
  assumes "X \<in> sets (Pi\<^sub>M J (\<lambda>_. M::'c measure))"
  shows "fm ` X \<in> sets (PiF (Collect finite) (\<lambda>_. M::'c measure))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fm ` X \<in> sets (Pi\<^sub>F (Collect finite) (\<lambda>_. M))
[PROOF STEP]
using fm_image_measurable[OF assms]
[PROOF STATE]
proof (prove)
using this:
fm ` X \<in> sets (Pi\<^sub>F {f ` J} (\<lambda>_. M))

goal (1 subgoal):
 1. fm ` X \<in> sets (Pi\<^sub>F (Collect finite) (\<lambda>_. M))
[PROOF STEP]
by (rule subspace_set_in_sets) (auto simp: finite_subset)


[STATEMENT]
lemma e_psp:
     "[| F \<in> A leadsTo[CC] A'; F \<in> B co B';
         \<forall>C\<in>CC. C Int B Int B' \<in> CC |]
      ==> F \<in> (A Int B') leadsTo[CC] ((A' Int B) Un (B' - B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<in> A leadsTo[CC] A'; F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC\<rbrakk> \<Longrightarrow> F \<in> (A \<inter> B') leadsTo[CC] (A' \<inter> B \<union> (B' - B))
[PROOF STEP]
apply (erule leadsETo_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>A Ba. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A ensures Ba; A - Ba \<in> insert {} CC\<rbrakk> \<Longrightarrow> F \<in> (A \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B))
 2. \<And>A Ba C. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A leadsTo[CC] Ba; F \<in> (A \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B)); F \<in> Ba leadsTo[CC] C; F \<in> (Ba \<inter> B') leadsTo[CC] (C \<inter> B \<union> (B' - B))\<rbrakk> \<Longrightarrow> F \<in> (A \<inter> B') leadsTo[CC] (C \<inter> B \<union> (B' - B))
 3. \<And>Ba S. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; \<forall>A\<in>S. F \<in> A leadsTo[CC] Ba \<and> F \<in> (A \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B))\<rbrakk> \<Longrightarrow> F \<in> (\<Union> S \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B))
[PROOF STEP]
prefer 3
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Ba S. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; \<forall>A\<in>S. F \<in> A leadsTo[CC] Ba \<and> F \<in> (A \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B))\<rbrakk> \<Longrightarrow> F \<in> (\<Union> S \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B))
 2. \<And>A Ba. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A ensures Ba; A - Ba \<in> insert {} CC\<rbrakk> \<Longrightarrow> F \<in> (A \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B))
 3. \<And>A Ba C. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A leadsTo[CC] Ba; F \<in> (A \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B)); F \<in> Ba leadsTo[CC] C; F \<in> (Ba \<inter> B') leadsTo[CC] (C \<inter> B \<union> (B' - B))\<rbrakk> \<Longrightarrow> F \<in> (A \<inter> B') leadsTo[CC] (C \<inter> B \<union> (B' - B))
[PROOF STEP]
apply (blast intro: leadsETo_Union_Int)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A Ba. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A ensures Ba; A - Ba \<in> insert {} CC\<rbrakk> \<Longrightarrow> F \<in> (A \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B))
 2. \<And>A Ba C. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A leadsTo[CC] Ba; F \<in> (A \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B)); F \<in> Ba leadsTo[CC] C; F \<in> (Ba \<inter> B') leadsTo[CC] (C \<inter> B \<union> (B' - B))\<rbrakk> \<Longrightarrow> F \<in> (A \<inter> B') leadsTo[CC] (C \<inter> B \<union> (B' - B))
[PROOF STEP]
apply (rule_tac [2] leadsETo_Un_duplicate2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A Ba. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A ensures Ba; A - Ba \<in> insert {} CC\<rbrakk> \<Longrightarrow> F \<in> (A \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B))
 2. \<And>A Ba C. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A leadsTo[CC] Ba; F \<in> (A \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B)); F \<in> Ba leadsTo[CC] C; F \<in> (Ba \<inter> B') leadsTo[CC] (C \<inter> B \<union> (B' - B))\<rbrakk> \<Longrightarrow> F \<in> (A \<inter> B') leadsTo[CC] (C \<inter> B \<union> (B' - B) \<union> (B' - B))
[PROOF STEP]
apply (erule_tac [2] leadsETo_cancel_Diff1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A Ba. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A ensures Ba; A - Ba \<in> insert {} CC\<rbrakk> \<Longrightarrow> F \<in> (A \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B))
 2. \<And>A Ba C. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A leadsTo[CC] Ba; F \<in> Ba leadsTo[CC] C; F \<in> (Ba \<inter> B') leadsTo[CC] (C \<inter> B \<union> (B' - B))\<rbrakk> \<Longrightarrow> F \<in> (Ba \<inter> B - (B' - B)) leadsTo[CC] (C \<inter> B \<union> (B' - B))
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A Ba C. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A leadsTo[CC] Ba; F \<in> Ba leadsTo[CC] C; F \<in> (Ba \<inter> B') leadsTo[CC] (C \<inter> B \<union> (B' - B))\<rbrakk> \<Longrightarrow> F \<in> (Ba \<inter> B - (B' - B)) leadsTo[CC] (C \<inter> B \<union> (B' - B))
 2. \<And>A Ba. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A ensures Ba; A - Ba \<in> insert {} CC\<rbrakk> \<Longrightarrow> F \<in> (A \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B))
[PROOF STEP]
apply (simp add: Int_Diff Diff_triv)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A Ba C. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A leadsTo[CC] Ba; F \<in> Ba leadsTo[CC] C; F \<in> (Ba \<inter> B') leadsTo[CC] (C \<inter> B \<union> (B' - B))\<rbrakk> \<Longrightarrow> F \<in> (Ba \<inter> B) leadsTo[CC] (C \<inter> B \<union> (B' - B))
 2. \<And>A Ba. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A ensures Ba; A - Ba \<in> insert {} CC\<rbrakk> \<Longrightarrow> F \<in> (A \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B))
[PROOF STEP]
apply (blast intro: leadsETo_weaken_L dest: constrains_imp_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A Ba. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A ensures Ba; A - Ba \<in> insert {} CC\<rbrakk> \<Longrightarrow> F \<in> (A \<inter> B') leadsTo[CC] (Ba \<inter> B \<union> (B' - B))
[PROOF STEP]
apply (rule leadsETo_Basis)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A Ba. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A ensures Ba; A - Ba \<in> insert {} CC\<rbrakk> \<Longrightarrow> F \<in> A \<inter> B' ensures Ba \<inter> B \<union> (B' - B)
 2. \<And>A Ba. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A ensures Ba; A - Ba \<in> insert {} CC\<rbrakk> \<Longrightarrow> A \<inter> B' - (Ba \<inter> B \<union> (B' - B)) \<in> insert {} CC
[PROOF STEP]
apply (blast intro: psp_ensures)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A Ba. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A ensures Ba; A - Ba \<in> insert {} CC\<rbrakk> \<Longrightarrow> A \<inter> B' - (Ba \<inter> B \<union> (B' - B)) \<in> insert {} CC
[PROOF STEP]
apply (subgoal_tac "A Int B' - (Ba Int B Un (B' - B)) = (A - Ba) Int B Int B'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A Ba. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A ensures Ba; A - Ba \<in> insert {} CC; A \<inter> B' - (Ba \<inter> B \<union> (B' - B)) = (A - Ba) \<inter> B \<inter> B'\<rbrakk> \<Longrightarrow> A \<inter> B' - (Ba \<inter> B \<union> (B' - B)) \<in> insert {} CC
 2. \<And>A Ba. \<lbrakk>F \<in> B co B'; \<forall>C\<in>CC. C \<inter> B \<inter> B' \<in> CC; F \<in> A ensures Ba; A - Ba \<in> insert {} CC\<rbrakk> \<Longrightarrow> A \<inter> B' - (Ba \<inter> B \<union> (B' - B)) = (A - Ba) \<inter> B \<inter> B'
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bij_betw_inv_into_twice:
assumes "bij_betw f A A'"
shows "\<forall>a \<in> A. inv_into A' (inv_into A f) a = f a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>A. inv_into A' (inv_into A f) a = f a
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in> A \<Longrightarrow> inv_into A' (inv_into A f) a = f a
[PROOF STEP]
let ?f' = "inv_into A f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in> A \<Longrightarrow> inv_into A' (inv_into A f) a = f a
[PROOF STEP]
let ?f'' = "inv_into A' ?f'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in> A \<Longrightarrow> inv_into A' (inv_into A f) a = f a
[PROOF STEP]
have 1: "bij_betw ?f' A' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (inv_into A f) A' A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bij_betw f A A'

goal (1 subgoal):
 1. bij_betw (inv_into A f) A' A
[PROOF STEP]
by (auto simp add: bij_betw_inv_into)
[PROOF STATE]
proof (state)
this:
bij_betw (inv_into A f) A' A

goal (1 subgoal):
 1. \<And>a. a \<in> A \<Longrightarrow> inv_into A' (inv_into A f) a = f a
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in> A \<Longrightarrow> inv_into A' (inv_into A f) a = f a
[PROOF STEP]
assume *: "a \<in> A"
[PROOF STATE]
proof (state)
this:
a \<in> A

goal (1 subgoal):
 1. \<And>a. a \<in> A \<Longrightarrow> inv_into A' (inv_into A f) a = f a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
[PROOF STEP]
obtain a' where 2: "a' \<in> A'" and 3: "?f' a' = a"
[PROOF STATE]
proof (prove)
using this:
a \<in> A

goal (1 subgoal):
 1. (\<And>a'. \<lbrakk>a' \<in> A'; inv_into A f a' = a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
a \<in> A
bij_betw (inv_into A f) A' A

goal (1 subgoal):
 1. (\<And>a'. \<lbrakk>a' \<in> A'; inv_into A f a' = a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
using this:
a \<in> A
inj_on (inv_into A f) A' \<and> inv_into A f ` A' = A

goal (1 subgoal):
 1. (\<And>a'. \<lbrakk>a' \<in> A'; inv_into A f a' = a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
a' \<in> A'
inv_into A f a' = a

goal (1 subgoal):
 1. \<And>a. a \<in> A \<Longrightarrow> inv_into A' (inv_into A f) a = f a
[PROOF STEP]
hence "?f'' a = a'"
[PROOF STATE]
proof (prove)
using this:
a' \<in> A'
inv_into A f a' = a

goal (1 subgoal):
 1. inv_into A' (inv_into A f) a = a'
[PROOF STEP]
using * 1 3
[PROOF STATE]
proof (prove)
using this:
a' \<in> A'
inv_into A f a' = a
a \<in> A
bij_betw (inv_into A f) A' A
inv_into A f a' = a

goal (1 subgoal):
 1. inv_into A' (inv_into A f) a = a'
[PROOF STEP]
by (auto simp add: bij_betw_inv_into_left)
[PROOF STATE]
proof (state)
this:
inv_into A' (inv_into A f) a = a'

goal (1 subgoal):
 1. \<And>a. a \<in> A \<Longrightarrow> inv_into A' (inv_into A f) a = f a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inv_into A' (inv_into A f) a = a'

goal (1 subgoal):
 1. \<And>a. a \<in> A \<Longrightarrow> inv_into A' (inv_into A f) a = f a
[PROOF STEP]
have "f a = a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a = a'
[PROOF STEP]
using assms 2 3
[PROOF STATE]
proof (prove)
using this:
bij_betw f A A'
a' \<in> A'
inv_into A f a' = a

goal (1 subgoal):
 1. f a = a'
[PROOF STEP]
by (auto simp add: bij_betw_inv_into_right)
[PROOF STATE]
proof (state)
this:
f a = a'

goal (1 subgoal):
 1. \<And>a. a \<in> A \<Longrightarrow> inv_into A' (inv_into A f) a = f a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inv_into A' (inv_into A f) a = a'
f a = a'
[PROOF STEP]
show "?f'' a = f a"
[PROOF STATE]
proof (prove)
using this:
inv_into A' (inv_into A f) a = a'
f a = a'

goal (1 subgoal):
 1. inv_into A' (inv_into A f) a = f a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inv_into A' (inv_into A f) a = f a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "VARS H x y z w
 {P ** Q}
 SKIP
 {Q ** P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {P ** Q}
SKIP
{Q ** P}
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>H x y z w. P ** Q \<Longrightarrow> Q ** P
[PROOF STEP]
apply(simp add: star_comm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done