[STATEMENT]
lemma spec_is_ringed_space:
  shows "ringed_space Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b
add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ringed_space Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
proof (intro ringed_space.intro)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
show "sheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b
     add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
using sheaf_spec_is_sheaf
[PROOF STATE]
proof (prove)
using this:
sheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec

goal (1 subgoal):
 1. sheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms \<O>b add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma get_lower_bound[intro]:
  assumes "U \<in> I" "V \<in> I"
  shows "get_lower_bound U V \<in> I" "get_lower_bound U V \<subseteq> U" "get_lower_bound U V \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_lower_bound U V \<in> I &&& get_lower_bound U V \<subseteq> U &&& get_lower_bound U V \<subseteq> V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. get_lower_bound U V \<in> I
 2. get_lower_bound U V \<subseteq> U
 3. get_lower_bound U V \<subseteq> V
[PROOF STEP]
have "\<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> V
[PROOF STEP]
using has_lower_bound[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<exists>W\<in>I. W \<subseteq> U \<inter> V

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

goal (3 subgoals):
 1. get_lower_bound U V \<in> I
 2. get_lower_bound U V \<subseteq> U
 3. get_lower_bound U V \<subseteq> V
[PROOF STEP]
from someI_ex[OF this]
[PROOF STATE]
proof (chain)
picking this:
(SOME x. x \<in> I \<and> x \<subseteq> U \<and> x \<subseteq> V) \<in> I \<and> (SOME x. x \<in> I \<and> x \<subseteq> U \<and> x \<subseteq> V) \<subseteq> U \<and> (SOME x. x \<in> I \<and> x \<subseteq> U \<and> x \<subseteq> V) \<subseteq> V
[PROOF STEP]
show "get_lower_bound U V \<in> I" "get_lower_bound U V \<subseteq> U" "get_lower_bound U V \<subseteq> V"
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> I \<and> x \<subseteq> U \<and> x \<subseteq> V) \<in> I \<and> (SOME x. x \<in> I \<and> x \<subseteq> U \<and> x \<subseteq> V) \<subseteq> U \<and> (SOME x. x \<in> I \<and> x \<subseteq> U \<and> x \<subseteq> V) \<subseteq> V

goal (1 subgoal):
 1. get_lower_bound U V \<in> I &&& get_lower_bound U V \<subseteq> U &&& get_lower_bound U V \<subseteq> V
[PROOF STEP]
unfolding get_lower_bound_def
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> I \<and> x \<subseteq> U \<and> x \<subseteq> V) \<in> I \<and> (SOME x. x \<in> I \<and> x \<subseteq> U \<and> x \<subseteq> V) \<subseteq> U \<and> (SOME x. x \<in> I \<and> x \<subseteq> U \<and> x \<subseteq> V) \<subseteq> V

goal (1 subgoal):
 1. (SOME W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> V) \<in> I &&& (SOME W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> V) \<subseteq> U &&& (SOME W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> V) \<subseteq> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
get_lower_bound U V \<in> I
get_lower_bound U V \<subseteq> U
get_lower_bound U V \<subseteq> V

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma obtain_lower_bound_finite:
  assumes "finite Us"  "Us \<noteq> {}" "Us \<subseteq> I"
  obtains W where "W \<in> I" "\<forall>U\<in>Us. W \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>W. \<lbrakk>W \<in> I; \<forall>U\<in>Us. W \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite Us
Us \<noteq> {}
Us \<subseteq> I

goal (1 subgoal):
 1. (\<And>W. \<lbrakk>W \<in> I; \<forall>U\<in>Us. W \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (induct Us arbitrary:thesis)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>thesis. \<lbrakk>\<And>W. \<lbrakk>W \<in> I; Ball {} ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; {} \<noteq> {}; {} \<subseteq> I\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x F thesis. \<lbrakk>finite F; x \<notin> F; \<And>thesis. \<lbrakk>\<And>W. \<lbrakk>W \<in> I; Ball F ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; F \<noteq> {}; F \<subseteq> I\<rbrakk> \<Longrightarrow> thesis; \<And>W. \<lbrakk>W \<in> I; Ball (insert x F) ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; insert x F \<noteq> {}; insert x F \<subseteq> I\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (insert U F)
[PROOF STATE]
proof (state)
this:
finite F
U \<notin> F
\<lbrakk>\<And>W. \<lbrakk>W \<in> I; \<forall>a\<in>F. W \<subseteq> a\<rbrakk> \<Longrightarrow> ?thesis1; F \<noteq> {}; F \<subseteq> I\<rbrakk> \<Longrightarrow> ?thesis1
\<lbrakk>?W1 \<in> I; \<forall>a\<in>insert U F. ?W1 \<subseteq> a\<rbrakk> \<Longrightarrow> thesis
insert U F \<noteq> {}
insert U F \<subseteq> I

goal (2 subgoals):
 1. \<And>thesis. \<lbrakk>\<And>W. \<lbrakk>W \<in> I; Ball {} ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; {} \<noteq> {}; {} \<subseteq> I\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x F thesis. \<lbrakk>finite F; x \<notin> F; \<And>thesis. \<lbrakk>\<And>W. \<lbrakk>W \<in> I; Ball F ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; F \<noteq> {}; F \<subseteq> I\<rbrakk> \<Longrightarrow> thesis; \<And>W. \<lbrakk>W \<in> I; Ball (insert x F) ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; insert x F \<noteq> {}; insert x F \<subseteq> I\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have ?case when "F={}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using insert.prems(1) insert.prems(3) that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?W1 \<in> I; \<forall>a\<in>insert U F. ?W1 \<subseteq> a\<rbrakk> \<Longrightarrow> thesis
insert U F \<subseteq> I
F = {}

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
F = {} \<Longrightarrow> thesis

goal (2 subgoals):
 1. \<And>thesis. \<lbrakk>\<And>W. \<lbrakk>W \<in> I; Ball {} ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; {} \<noteq> {}; {} \<subseteq> I\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x F thesis. \<lbrakk>finite F; x \<notin> F; \<And>thesis. \<lbrakk>\<And>W. \<lbrakk>W \<in> I; Ball F ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; F \<noteq> {}; F \<subseteq> I\<rbrakk> \<Longrightarrow> thesis; \<And>W. \<lbrakk>W \<in> I; Ball (insert x F) ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; insert x F \<noteq> {}; insert x F \<subseteq> I\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
F = {} \<Longrightarrow> thesis

goal (2 subgoals):
 1. \<And>thesis. \<lbrakk>\<And>W. \<lbrakk>W \<in> I; Ball {} ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; {} \<noteq> {}; {} \<subseteq> I\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x F thesis. \<lbrakk>finite F; x \<notin> F; \<And>thesis. \<lbrakk>\<And>W. \<lbrakk>W \<in> I; Ball F ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; F \<noteq> {}; F \<subseteq> I\<rbrakk> \<Longrightarrow> thesis; \<And>W. \<lbrakk>W \<in> I; Ball (insert x F) ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; insert x F \<noteq> {}; insert x F \<subseteq> I\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have ?case when "F\<noteq>{}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
obtain W where "W \<in> I" "\<forall>U\<in>F. W \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>W. \<lbrakk>W \<in> I; \<forall>U\<in>F. W \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using insert.hyps(3) insert.prems(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>W. \<lbrakk>W \<in> I; \<forall>a\<in>F. W \<subseteq> a\<rbrakk> \<Longrightarrow> ?thesis1; F \<noteq> {}; F \<subseteq> I\<rbrakk> \<Longrightarrow> ?thesis1
insert U F \<subseteq> I

goal (1 subgoal):
 1. (\<And>W. \<lbrakk>W \<in> I; \<forall>U\<in>F. W \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
W \<in> I
\<forall>U\<in>F. W \<subseteq> U

goal (1 subgoal):
 1. thesis
[PROOF STEP]
obtain W1 where "W1 \<in>I" "W1 \<subseteq> U" "W1 \<subseteq> W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>W1. \<lbrakk>W1 \<in> I; W1 \<subseteq> U; W1 \<subseteq> W\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson \<open>W \<in> I\<close> get_lower_bound(1) get_lower_bound(2) get_lower_bound(3)
          insert.prems(3) insert_subset)
[PROOF STATE]
proof (state)
this:
W1 \<in> I
W1 \<subseteq> U
W1 \<subseteq> W

goal (1 subgoal):
 1. thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
W1 \<in> I
W1 \<subseteq> U
W1 \<subseteq> W
[PROOF STEP]
have "\<forall>a\<in>insert U F. W1 \<subseteq> a"
[PROOF STATE]
proof (prove)
using this:
W1 \<in> I
W1 \<subseteq> U
W1 \<subseteq> W

goal (1 subgoal):
 1. \<forall>a\<in>insert U F. W1 \<subseteq> a
[PROOF STEP]
using \<open>\<forall>U\<in>F. W \<subseteq> U\<close>
[PROOF STATE]
proof (prove)
using this:
W1 \<in> I
W1 \<subseteq> U
W1 \<subseteq> W
\<forall>U\<in>F. W \<subseteq> U

goal (1 subgoal):
 1. \<forall>a\<in>insert U F. W1 \<subseteq> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>insert U F. W1 \<subseteq> a

goal (1 subgoal):
 1. thesis
[PROOF STEP]
with \<open>W1 \<in>I\<close>
[PROOF STATE]
proof (chain)
picking this:
W1 \<in> I
\<forall>a\<in>insert U F. W1 \<subseteq> a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
W1 \<in> I
\<forall>a\<in>insert U F. W1 \<subseteq> a

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using insert(4)
[PROOF STATE]
proof (prove)
using this:
W1 \<in> I
\<forall>a\<in>insert U F. W1 \<subseteq> a
\<lbrakk>?W1 \<in> I; \<forall>a\<in>insert U F. ?W1 \<subseteq> a\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
F \<noteq> {} \<Longrightarrow> thesis

goal (2 subgoals):
 1. \<And>thesis. \<lbrakk>\<And>W. \<lbrakk>W \<in> I; Ball {} ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; {} \<noteq> {}; {} \<subseteq> I\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x F thesis. \<lbrakk>finite F; x \<notin> F; \<And>thesis. \<lbrakk>\<And>W. \<lbrakk>W \<in> I; Ball F ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; F \<noteq> {}; F \<subseteq> I\<rbrakk> \<Longrightarrow> thesis; \<And>W. \<lbrakk>W \<in> I; Ball (insert x F) ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; insert x F \<noteq> {}; insert x F \<subseteq> I\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
F = {} \<Longrightarrow> thesis
F \<noteq> {} \<Longrightarrow> thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
F = {} \<Longrightarrow> thesis
F \<noteq> {} \<Longrightarrow> thesis

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

goal (1 subgoal):
 1. \<And>thesis. \<lbrakk>\<And>W. \<lbrakk>W \<in> I; Ball {} ((\<subseteq>) W)\<rbrakk> \<Longrightarrow> thesis; {} \<noteq> {}; {} \<subseteq> I\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
qed simp


[STATEMENT]
lemma eventually_principal_subs: "eventually P (principal_subs As A) \<longleftrightarrow> (\<forall>x. x\<in>As \<and> x\<subseteq>A \<longrightarrow> P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually P (principal_subs As A) = (\<forall>x. x \<in> As \<and> x \<subseteq> A \<longrightarrow> P x)
[PROOF STEP]
unfolding principal_subs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually P (Abs_filter (\<lambda>P. \<forall>x. x \<in> As \<and> x \<subseteq> A \<longrightarrow> P x)) = (\<forall>x. x \<in> As \<and> x \<subseteq> A \<longrightarrow> P x)
[PROOF STEP]
by (rule eventually_Abs_filter, rule is_filter.intro) auto


[STATEMENT]
lemma principal_subs_UNIV[simp]: "principal_subs UNIV UNIV = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. principal_subs UNIV UNIV = top
[PROOF STEP]
by (auto simp: filter_eq_iff eventually_principal_subs)


[STATEMENT]
lemma principal_subs_empty[simp]: "principal_subs {} s = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. principal_subs {} s = bot
[PROOF STEP]
(*"principal_subs ss {} = bot"*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. principal_subs {} s = bot
[PROOF STEP]
by (auto simp: filter_eq_iff eventually_principal_subs)


[STATEMENT]
lemma principal_subs_le_iff[iff]:
  "principal_subs As A \<le> principal_subs As' A'
            \<longleftrightarrow> {x. x\<in>As \<and> x \<subseteq> A} \<subseteq> {x. x\<in>As' \<and> x \<subseteq> A'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (principal_subs As A \<le> principal_subs As' A') = ({x \<in> As. x \<subseteq> A} \<subseteq> {x \<in> As'. x \<subseteq> A'})
[PROOF STEP]
unfolding le_filter_def eventually_principal_subs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>P. (\<forall>x. x \<in> As' \<and> x \<subseteq> A' \<longrightarrow> P x) \<longrightarrow> (\<forall>x. x \<in> As \<and> x \<subseteq> A \<longrightarrow> P x)) = ({x \<in> As. x \<subseteq> A} \<subseteq> {x \<in> As'. x \<subseteq> A'})
[PROOF STEP]
by blast


[STATEMENT]
lemma principal_subs_eq_iff[iff]:
    "principal_subs As A = principal_subs As' A' \<longleftrightarrow>{x. x\<in>As \<and> x \<subseteq> A} = {x. x\<in>As' \<and> x \<subseteq> A'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (principal_subs As A = principal_subs As' A') = ({x \<in> As. x \<subseteq> A} = {x \<in> As'. x \<subseteq> A'})
[PROOF STEP]
unfolding eq_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (principal_subs As A \<le> principal_subs As' A' \<and> principal_subs As' A' \<le> principal_subs As A) \<le> ({x \<in> As. x \<subseteq> A} \<subseteq> {x \<in> As'. x \<subseteq> A'} \<and> {x \<in> As'. x \<subseteq> A'} \<subseteq> {x \<in> As. x \<subseteq> A}) \<and> ({x \<in> As. x \<subseteq> A} \<subseteq> {x \<in> As'. x \<subseteq> A'} \<and> {x \<in> As'. x \<subseteq> A'} \<subseteq> {x \<in> As. x \<subseteq> A}) \<le> (principal_subs As A \<le> principal_subs As' A' \<and> principal_subs As' A' \<le> principal_subs As A)
[PROOF STEP]
by simp


[STATEMENT]
lemma principal_subs_inj_on[simp]:"inj_on (principal_subs As) As"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (principal_subs As) As
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>As. \<forall>y\<in>As. principal_subs As x = principal_subs As y \<longrightarrow> x = y
[PROOF STEP]
by auto


[STATEMENT]
lemma eventually_lbound_finite:
  assumes "finite A" "A\<noteq>{}" "A\<subseteq>I"
  shows "(\<forall>\<^sub>F w in lbound A. P w) \<longleftrightarrow> (\<exists>w0. w0 \<in> I \<and> (\<forall>a\<in>A. w0 \<subseteq> a) \<and> (\<forall>w. (w\<subseteq>w0 \<and> w\<in>I) \<longrightarrow> P w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually P (lbound A) = (\<exists>w0. w0 \<in> I \<and> (\<forall>a\<in>A. w0 \<subseteq> a) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eventually P (lbound A) = (\<exists>w0. w0 \<in> I \<and> (\<forall>a\<in>A. w0 \<subseteq> a) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))
[PROOF STEP]
have "\<exists>x. x \<in> I \<and> (\<forall>xa\<in>A. x \<subseteq> xa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> I \<and> (\<forall>xa\<in>A. x \<subseteq> xa)
[PROOF STEP]
by (metis Int_iff assms inf.order_iff obtain_lower_bound_finite)
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> I \<and> (\<forall>xa\<in>A. x \<subseteq> xa)

goal (1 subgoal):
 1. eventually P (lbound A) = (\<exists>w0. w0 \<in> I \<and> (\<forall>a\<in>A. w0 \<subseteq> a) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> I \<and> (\<forall>xa\<in>A. x \<subseteq> xa)

goal (1 subgoal):
 1. eventually P (lbound A) = (\<exists>w0. w0 \<in> I \<and> (\<forall>a\<in>A. w0 \<subseteq> a) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))
[PROOF STEP]
have " \<exists>x. x \<in> I \<and> Ball A ((\<subseteq>) x)
              \<and> {xa \<in> I. xa \<subseteq> x} \<subseteq> {x \<in> I. x \<subseteq> a}
                \<and> {xa \<in> I. xa \<subseteq> x} \<subseteq> {x \<in> I. x \<subseteq> b}"
    if "a \<in> I \<and> (\<forall>x\<in>A. a \<subseteq> x)" "b \<in> I \<and> (\<forall>x\<in>A. b \<subseteq> x)" for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> I \<and> Ball A ((\<subseteq>) x) \<and> {xa \<in> I. xa \<subseteq> x} \<subseteq> {x \<in> I. x \<subseteq> a} \<and> {xa \<in> I. xa \<subseteq> x} \<subseteq> {x \<in> I. x \<subseteq> b}
[PROOF STEP]
apply (rule exI[where x="get_lower_bound a b"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_lower_bound a b \<in> I \<and> Ball A ((\<subseteq>) (get_lower_bound a b)) \<and> {xa \<in> I. xa \<subseteq> get_lower_bound a b} \<subseteq> {x \<in> I. x \<subseteq> a} \<and> {xa \<in> I. xa \<subseteq> get_lower_bound a b} \<subseteq> {x \<in> I. x \<subseteq> b}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in> I \<and> (\<forall>x\<in>A. a \<subseteq> x)
b \<in> I \<and> (\<forall>x\<in>A. b \<subseteq> x)

goal (1 subgoal):
 1. get_lower_bound a b \<in> I \<and> Ball A ((\<subseteq>) (get_lower_bound a b)) \<and> {xa \<in> I. xa \<subseteq> get_lower_bound a b} \<subseteq> {x \<in> I. x \<subseteq> a} \<and> {xa \<in> I. xa \<subseteq> get_lower_bound a b} \<subseteq> {x \<in> I. x \<subseteq> b}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>a \<in> I; \<forall>x\<in>A. a \<subseteq> x; b \<in> I; \<forall>x\<in>A. b \<subseteq> x; x \<in> A; xa \<in> get_lower_bound a b\<rbrakk> \<Longrightarrow> xa \<in> x
 2. \<And>x xa. \<lbrakk>a \<in> I; \<forall>x\<in>A. a \<subseteq> x; b \<in> I; \<forall>x\<in>A. b \<subseteq> x; x \<in> I; x \<subseteq> get_lower_bound a b; xa \<in> x\<rbrakk> \<Longrightarrow> xa \<in> a
 3. \<And>x xa. \<lbrakk>a \<in> I; \<forall>x\<in>A. a \<subseteq> x; b \<in> I; \<forall>x\<in>A. b \<subseteq> x; x \<in> I; x \<subseteq> get_lower_bound a b; xa \<in> x\<rbrakk> \<Longrightarrow> xa \<in> b
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> I; \<forall>x\<in>A. a \<subseteq> x; b \<in> I; \<forall>x\<in>A. b \<subseteq> x; x_ \<in> A; xa_ \<in> get_lower_bound a b\<rbrakk> \<Longrightarrow> xa_ \<in> x_
[PROOF STEP]
using get_lower_bound(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?U \<in> I; ?V \<in> I\<rbrakk> \<Longrightarrow> get_lower_bound ?U ?V \<subseteq> ?U

goal (1 subgoal):
 1. \<lbrakk>a \<in> I; \<forall>x\<in>A. a \<subseteq> x; b \<in> I; \<forall>x\<in>A. b \<subseteq> x; x_ \<in> A; xa_ \<in> get_lower_bound a b\<rbrakk> \<Longrightarrow> xa_ \<in> x_
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>a \<in> I; \<forall>x\<in>A. a \<subseteq> x; b \<in> I; \<forall>x\<in>A. b \<subseteq> x; x \<in> I; x \<subseteq> get_lower_bound a b; xa \<in> x\<rbrakk> \<Longrightarrow> xa \<in> a
 2. \<And>x xa. \<lbrakk>a \<in> I; \<forall>x\<in>A. a \<subseteq> x; b \<in> I; \<forall>x\<in>A. b \<subseteq> x; x \<in> I; x \<subseteq> get_lower_bound a b; xa \<in> x\<rbrakk> \<Longrightarrow> xa \<in> b
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> I; \<forall>x\<in>A. a \<subseteq> x; b \<in> I; \<forall>x\<in>A. b \<subseteq> x; x_ \<in> I; x_ \<subseteq> get_lower_bound a b; xa_ \<in> x_\<rbrakk> \<Longrightarrow> xa_ \<in> a
[PROOF STEP]
by (meson get_lower_bound(2) subsetD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>a \<in> I; \<forall>x\<in>A. a \<subseteq> x; b \<in> I; \<forall>x\<in>A. b \<subseteq> x; x \<in> I; x \<subseteq> get_lower_bound a b; xa \<in> x\<rbrakk> \<Longrightarrow> xa \<in> b
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> I; \<forall>x\<in>A. a \<subseteq> x; b \<in> I; \<forall>x\<in>A. b \<subseteq> x; x_ \<in> I; x_ \<subseteq> get_lower_bound a b; xa_ \<in> x_\<rbrakk> \<Longrightarrow> xa_ \<in> b
[PROOF STEP]
by (meson get_lower_bound(3) subsetD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a1 \<in> I \<and> (\<forall>x\<in>A. ?a1 \<subseteq> x); ?b1 \<in> I \<and> (\<forall>x\<in>A. ?b1 \<subseteq> x)\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> Ball A ((\<subseteq>) x) \<and> {xa \<in> I. xa \<subseteq> x} \<subseteq> {x \<in> I. x \<subseteq> ?a1} \<and> {xa \<in> I. xa \<subseteq> x} \<subseteq> {x \<in> I. x \<subseteq> ?b1}

goal (1 subgoal):
 1. eventually P (lbound A) = (\<exists>w0. w0 \<in> I \<and> (\<forall>a\<in>A. w0 \<subseteq> a) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a1 \<in> I \<and> (\<forall>x\<in>A. ?a1 \<subseteq> x); ?b1 \<in> I \<and> (\<forall>x\<in>A. ?b1 \<subseteq> x)\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> Ball A ((\<subseteq>) x) \<and> {xa \<in> I. xa \<subseteq> x} \<subseteq> {x \<in> I. x \<subseteq> ?a1} \<and> {xa \<in> I. xa \<subseteq> x} \<subseteq> {x \<in> I. x \<subseteq> ?b1}

goal (1 subgoal):
 1. eventually P (lbound A) = (\<exists>w0. w0 \<in> I \<and> (\<forall>a\<in>A. w0 \<subseteq> a) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))
[PROOF STEP]
have "(\<exists>b\<in>{S \<in> I. Ball A ((\<subseteq>) S)}. eventually P (principal_subs I b)) =
    (\<exists>w0. w0 \<in> I \<and> Ball A ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>b\<in>{S \<in> I. Ball A ((\<subseteq>) S)}. eventually P (principal_subs I b)) = (\<exists>w0. w0 \<in> I \<and> Ball A ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))
[PROOF STEP]
unfolding eventually_principal_subs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>b\<in>{S \<in> I. Ball A ((\<subseteq>) S)}. \<forall>x. x \<in> I \<and> x \<subseteq> b \<longrightarrow> P x) = (\<exists>w0. w0 \<in> I \<and> Ball A ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<exists>b\<in>{S \<in> I. Ball A ((\<subseteq>) S)}. eventually P (principal_subs I b)) = (\<exists>w0. w0 \<in> I \<and> Ball A ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))

goal (1 subgoal):
 1. eventually P (lbound A) = (\<exists>w0. w0 \<in> I \<and> (\<forall>a\<in>A. w0 \<subseteq> a) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> I \<and> (\<forall>xa\<in>A. x \<subseteq> xa)
\<lbrakk>?a1 \<in> I \<and> (\<forall>x\<in>A. ?a1 \<subseteq> x); ?b1 \<in> I \<and> (\<forall>x\<in>A. ?b1 \<subseteq> x)\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> Ball A ((\<subseteq>) x) \<and> {xa \<in> I. xa \<subseteq> x} \<subseteq> {x \<in> I. x \<subseteq> ?a1} \<and> {xa \<in> I. xa \<subseteq> x} \<subseteq> {x \<in> I. x \<subseteq> ?b1}
(\<exists>b\<in>{S \<in> I. Ball A ((\<subseteq>) S)}. eventually P (principal_subs I b)) = (\<exists>w0. w0 \<in> I \<and> Ball A ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> I \<and> (\<forall>xa\<in>A. x \<subseteq> xa)
\<lbrakk>?a1 \<in> I \<and> (\<forall>x\<in>A. ?a1 \<subseteq> x); ?b1 \<in> I \<and> (\<forall>x\<in>A. ?b1 \<subseteq> x)\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> Ball A ((\<subseteq>) x) \<and> {xa \<in> I. xa \<subseteq> x} \<subseteq> {x \<in> I. x \<subseteq> ?a1} \<and> {xa \<in> I. xa \<subseteq> x} \<subseteq> {x \<in> I. x \<subseteq> ?b1}
(\<exists>b\<in>{S \<in> I. Ball A ((\<subseteq>) S)}. eventually P (principal_subs I b)) = (\<exists>w0. w0 \<in> I \<and> Ball A ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))

goal (1 subgoal):
 1. eventually P (lbound A) = (\<exists>w0. w0 \<in> I \<and> (\<forall>a\<in>A. w0 \<subseteq> a) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))
[PROOF STEP]
unfolding lbound_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> I \<and> (\<forall>xa\<in>A. x \<subseteq> xa)
\<lbrakk>?a1 \<in> I \<and> (\<forall>x\<in>A. ?a1 \<subseteq> x); ?b1 \<in> I \<and> (\<forall>x\<in>A. ?b1 \<subseteq> x)\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> I \<and> Ball A ((\<subseteq>) x) \<and> {xa \<in> I. xa \<subseteq> x} \<subseteq> {x \<in> I. x \<subseteq> ?a1} \<and> {xa \<in> I. xa \<subseteq> x} \<subseteq> {x \<in> I. x \<subseteq> ?b1}
(\<exists>b\<in>{S \<in> I. Ball A ((\<subseteq>) S)}. eventually P (principal_subs I b)) = (\<exists>w0. w0 \<in> I \<and> Ball A ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))

goal (1 subgoal):
 1. eventually P (Inf (principal_subs I ` {S \<in> I. Ball A ((\<subseteq>) S)})) = (\<exists>w0. w0 \<in> I \<and> (\<forall>a\<in>A. w0 \<subseteq> a) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))
[PROOF STEP]
by (subst eventually_INF_base) auto
[PROOF STATE]
proof (state)
this:
eventually P (lbound A) = (\<exists>w0. w0 \<in> I \<and> (\<forall>a\<in>A. w0 \<subseteq> a) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lbound_eq:
  assumes A:"finite A" "A\<noteq>{}" "A\<subseteq>I"
  assumes B:"finite B" "B\<noteq>{}" "B\<subseteq>I"
  shows "lbound A = lbound B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lbound A = lbound B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lbound A = lbound B
[PROOF STEP]
have "eventually P (lbound A')" if "eventually P (lbound B')"
    and A':"finite A'" "A'\<noteq>{}" "A' \<subseteq> I"
    and B':"finite B'" "B'\<noteq>{}" "B' \<subseteq> I"
  for P A' B'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually P (lbound A')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eventually P (lbound A')
[PROOF STEP]
obtain w0 where w0:"w0 \<in> I" "(\<forall>a\<in>B'. w0 \<subseteq> a)" "(\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>w0. \<lbrakk>w0 \<in> I; \<forall>a\<in>B'. w0 \<subseteq> a; \<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>eventually P (lbound B')\<close>
[PROOF STATE]
proof (prove)
using this:
eventually P (lbound B')

goal (1 subgoal):
 1. (\<And>w0. \<lbrakk>w0 \<in> I; \<forall>a\<in>B'. w0 \<subseteq> a; \<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding eventually_lbound_finite[OF B',of P]
[PROOF STATE]
proof (prove)
using this:
\<exists>w0. w0 \<in> I \<and> Ball B' ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w)

goal (1 subgoal):
 1. (\<And>w0. \<lbrakk>w0 \<in> I; \<forall>a\<in>B'. w0 \<subseteq> a; \<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w0 \<in> I
\<forall>a\<in>B'. w0 \<subseteq> a
\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w

goal (1 subgoal):
 1. eventually P (lbound A')
[PROOF STEP]
obtain w1 where w1:"w1 \<in> I" "\<forall>U\<in>A'. w1 \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>w1. \<lbrakk>w1 \<in> I; \<forall>U\<in>A'. w1 \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obtain_lower_bound_finite[OF A']
[PROOF STATE]
proof (prove)
using this:
(\<And>W. \<lbrakk>W \<in> I; \<forall>U\<in>A'. W \<subseteq> U\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>w1. \<lbrakk>w1 \<in> I; \<forall>U\<in>A'. w1 \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w1 \<in> I
\<forall>U\<in>A'. w1 \<subseteq> U

goal (1 subgoal):
 1. eventually P (lbound A')
[PROOF STEP]
define w2 where "w2=get_lower_bound w0 w1"
[PROOF STATE]
proof (state)
this:
w2 = get_lower_bound w0 w1

goal (1 subgoal):
 1. eventually P (lbound A')
[PROOF STEP]
have "w2 \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w2 \<in> I
[PROOF STEP]
using \<open>w0 \<in> I\<close> \<open>w1 \<in> I\<close>
[PROOF STATE]
proof (prove)
using this:
w0 \<in> I
w1 \<in> I

goal (1 subgoal):
 1. w2 \<in> I
[PROOF STEP]
unfolding w2_def
[PROOF STATE]
proof (prove)
using this:
w0 \<in> I
w1 \<in> I

goal (1 subgoal):
 1. get_lower_bound w0 w1 \<in> I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w2 \<in> I

goal (1 subgoal):
 1. eventually P (lbound A')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
w2 \<in> I

goal (1 subgoal):
 1. eventually P (lbound A')
[PROOF STEP]
have "\<forall>a\<in>A'. w2 \<subseteq> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>A'. w2 \<subseteq> a
[PROOF STEP]
unfolding w2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>A'. get_lower_bound w0 w1 \<subseteq> a
[PROOF STEP]
by (meson dual_order.trans get_lower_bound(3) w0(1) w1(1) w1(2))
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>A'. w2 \<subseteq> a

goal (1 subgoal):
 1. eventually P (lbound A')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>A'. w2 \<subseteq> a

goal (1 subgoal):
 1. eventually P (lbound A')
[PROOF STEP]
have "\<forall>w. w \<subseteq> w2 \<and> w \<in> I \<longrightarrow> P w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. w \<subseteq> w2 \<and> w \<in> I \<longrightarrow> P w
[PROOF STEP]
unfolding w2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. w \<subseteq> get_lower_bound w0 w1 \<and> w \<in> I \<longrightarrow> P w
[PROOF STEP]
by (meson dual_order.trans get_lower_bound(2) w0(1) w0(3) w1(1))
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<subseteq> w2 \<and> w \<in> I \<longrightarrow> P w

goal (1 subgoal):
 1. eventually P (lbound A')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
w2 \<in> I
\<forall>a\<in>A'. w2 \<subseteq> a
\<forall>w. w \<subseteq> w2 \<and> w \<in> I \<longrightarrow> P w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w2 \<in> I
\<forall>a\<in>A'. w2 \<subseteq> a
\<forall>w. w \<subseteq> w2 \<and> w \<in> I \<longrightarrow> P w

goal (1 subgoal):
 1. eventually P (lbound A')
[PROOF STEP]
unfolding eventually_lbound_finite[OF A',of P]
[PROOF STATE]
proof (prove)
using this:
w2 \<in> I
\<forall>a\<in>A'. w2 \<subseteq> a
\<forall>w. w \<subseteq> w2 \<and> w \<in> I \<longrightarrow> P w

goal (1 subgoal):
 1. \<exists>w0. w0 \<in> I \<and> Ball A' ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> P w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eventually P (lbound A')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>eventually ?P1 (lbound ?B'1); finite ?A'1; ?A'1 \<noteq> {}; ?A'1 \<subseteq> I; finite ?B'1; ?B'1 \<noteq> {}; ?B'1 \<subseteq> I\<rbrakk> \<Longrightarrow> eventually ?P1 (lbound ?A'1)

goal (1 subgoal):
 1. lbound A = lbound B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>eventually ?P1 (lbound ?B'1); finite ?A'1; ?A'1 \<noteq> {}; ?A'1 \<subseteq> I; finite ?B'1; ?B'1 \<noteq> {}; ?B'1 \<subseteq> I\<rbrakk> \<Longrightarrow> eventually ?P1 (lbound ?A'1)
[PROOF STEP]
have "eventually P (lbound A) = eventually P (lbound B)" for P
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>eventually ?P1 (lbound ?B'1); finite ?A'1; ?A'1 \<noteq> {}; ?A'1 \<subseteq> I; finite ?B'1; ?B'1 \<noteq> {}; ?B'1 \<subseteq> I\<rbrakk> \<Longrightarrow> eventually ?P1 (lbound ?A'1)

goal (1 subgoal):
 1. eventually P (lbound A) = eventually P (lbound B)
[PROOF STEP]
using A B
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>eventually ?P1 (lbound ?B'1); finite ?A'1; ?A'1 \<noteq> {}; ?A'1 \<subseteq> I; finite ?B'1; ?B'1 \<noteq> {}; ?B'1 \<subseteq> I\<rbrakk> \<Longrightarrow> eventually ?P1 (lbound ?A'1)
finite A
A \<noteq> {}
A \<subseteq> I
finite B
B \<noteq> {}
B \<subseteq> I

goal (1 subgoal):
 1. eventually P (lbound A) = eventually P (lbound B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eventually ?P1 (lbound A) = eventually ?P1 (lbound B)

goal (1 subgoal):
 1. lbound A = lbound B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eventually ?P1 (lbound A) = eventually ?P1 (lbound B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eventually ?P1 (lbound A) = eventually ?P1 (lbound B)

goal (1 subgoal):
 1. lbound A = lbound B
[PROOF STEP]
unfolding filter_eq_iff
[PROOF STATE]
proof (prove)
using this:
eventually ?P1 (lbound A) = eventually ?P1 (lbound B)

goal (1 subgoal):
 1. \<forall>P. eventually P (lbound A) = eventually P (lbound B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lbound A = lbound B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lbound_leq:
  assumes "A \<subseteq> B"
  shows "lbound A \<le>lbound B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lbound A \<le> lbound B
[PROOF STEP]
unfolding lbound_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf (principal_subs I ` {S \<in> I. Ball A ((\<subseteq>) S)}) \<le> Inf (principal_subs I ` {S \<in> I. Ball B ((\<subseteq>) S)})
[PROOF STEP]
apply (rule Inf_superset_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. principal_subs I ` {S \<in> I. Ball B ((\<subseteq>) S)} \<subseteq> principal_subs I ` {S \<in> I. Ball A ((\<subseteq>) S)}
[PROOF STEP]
apply (rule image_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {S \<in> I. Ball B ((\<subseteq>) S)} \<subseteq> {S \<in> I. Ball A ((\<subseteq>) S)}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> B

goal (1 subgoal):
 1. {S \<in> I. Ball B ((\<subseteq>) S)} \<subseteq> {S \<in> I. Ball A ((\<subseteq>) S)}
[PROOF STEP]
by auto


[STATEMENT]
lemma llbound_not_bot:
  assumes "I\<noteq> {}"
  shows "llbound \<noteq> bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llbound \<noteq> bot
[PROOF STEP]
unfolding trivial_limit_def llbound_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>\<^sub>F x in lbound {SOME a. a \<in> I}. False)
[PROOF STEP]
apply (subst eventually_lbound_finite)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. finite {SOME a. a \<in> I}
 2. {SOME a. a \<in> I} \<noteq> {}
 3. {SOME a. a \<in> I} \<subseteq> I
 4. \<nexists>w0. w0 \<in> I \<and> Ball {SOME a. a \<in> I} ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> False)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
I \<noteq> {}

goal (4 subgoals):
 1. finite {SOME a. a \<in> I}
 2. {SOME a. a \<in> I} \<noteq> {}
 3. {SOME a. a \<in> I} \<subseteq> I
 4. \<nexists>w0. w0 \<in> I \<and> Ball {SOME a. a \<in> I} ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> False)
[PROOF STEP]
by (auto simp add: some_in_eq)


[STATEMENT]
lemma llbound_lbound:
  assumes "finite A" "A\<noteq>{}" "A\<subseteq>I"
  shows "lbound A = llbound"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lbound A = llbound
[PROOF STEP]
unfolding llbound_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lbound A = lbound {SOME a. a \<in> I}
[PROOF STEP]
apply (rule lbound_eq)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. finite A
 2. A \<noteq> {}
 3. A \<subseteq> I
 4. finite {SOME a. a \<in> I}
 5. {SOME a. a \<in> I} \<noteq> {}
 6. {SOME a. a \<in> I} \<subseteq> I
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
A \<noteq> {}
A \<subseteq> I

goal (6 subgoals):
 1. finite A
 2. A \<noteq> {}
 3. A \<subseteq> I
 4. finite {SOME a. a \<in> I}
 5. {SOME a. a \<in> I} \<noteq> {}
 6. {SOME a. a \<in> I} \<subseteq> I
[PROOF STEP]
by (auto simp add: some_in_eq)


[STATEMENT]
lemma rel_is_equivalence:
  shows "equivalence (Sigma I \<FF>) {(x, y). x \<sim> y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalence (Sigma I \<FF>) {(x, y). x \<sim> y}
[PROOF STEP]
unfolding equivalence_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({(x, y). x \<sim> y} \<subseteq> Sigma I \<FF> \<times> Sigma I \<FF> \<and> (\<forall>a. a \<in> Sigma I \<FF> \<longrightarrow> (a, a) \<in> {(x, y). x \<sim> y})) \<and> (\<forall>a b. (a, b) \<in> {(x, y). x \<sim> y} \<longrightarrow> (b, a) \<in> {(x, y). x \<sim> y}) \<and> (\<forall>a b c. (a, b) \<in> {(x, y). x \<sim> y} \<longrightarrow> (b, c) \<in> {(x, y). x \<sim> y} \<longrightarrow> (a, c) \<in> {(x, y). x \<sim> y})
[PROOF STEP]
proof (intro conjI strip)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. {(x, y). x \<sim> y} \<subseteq> Sigma I \<FF> \<times> Sigma I \<FF>
 2. \<And>a. a \<in> Sigma I \<FF> \<Longrightarrow> (a, a) \<in> {(x, y). x \<sim> y}
 3. \<And>a b. (a, b) \<in> {(x, y). x \<sim> y} \<Longrightarrow> (b, a) \<in> {(x, y). x \<sim> y}
 4. \<And>a b c. \<lbrakk>(a, b) \<in> {(x, y). x \<sim> y}; (b, c) \<in> {(x, y). x \<sim> y}\<rbrakk> \<Longrightarrow> (a, c) \<in> {(x, y). x \<sim> y}
[PROOF STEP]
show "(a, c) \<in> {(x, y). x \<sim> y}"
    if "(a, b) \<in> {(x, y). x \<sim> y}" "(b, c) \<in> {(x, y). x \<sim> y}" for a b c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, c) \<in> {(x, y). x \<sim> y}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a, c) \<in> {(x, y). x \<sim> y}
[PROOF STEP]
obtain W1 where W1:"fst a \<in> I" "fst b \<in> I" "snd a \<in> \<FF> (fst a)" "snd b \<in> \<FF> (fst b)"
                    "W1 \<in> I" "W1 \<subseteq> fst a" "W1 \<subseteq> fst b"
                    "\<rho> (fst a) W1 (snd a) = \<rho> (fst b) W1 (snd b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>W1. \<lbrakk>fst a \<in> I; fst b \<in> I; snd a \<in> \<FF> (fst a); snd b \<in> \<FF> (fst b); W1 \<in> I; W1 \<subseteq> fst a; W1 \<subseteq> fst b; \<rho> (fst a) W1 (snd a) = \<rho> (fst b) W1 (snd b)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>(a, b) \<in> {(x, y). x \<sim> y}\<close>
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> {(x, y). x \<sim> y}

goal (1 subgoal):
 1. (\<And>W1. \<lbrakk>fst a \<in> I; fst b \<in> I; snd a \<in> \<FF> (fst a); snd b \<in> \<FF> (fst b); W1 \<in> I; W1 \<subseteq> fst a; W1 \<subseteq> fst b; \<rho> (fst a) W1 (snd a) = \<rho> (fst b) W1 (snd b)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding rel_def
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> {(x, y). (fst x \<in> I \<and> fst y \<in> I) \<and> (snd x \<in> \<FF> (fst x) \<and> snd y \<in> \<FF> (fst y)) \<and> (\<exists>W. W \<in> I \<and> W \<subseteq> fst x \<inter> fst y \<and> \<rho> (fst x) W (snd x) = \<rho> (fst y) W (snd y))}

goal (1 subgoal):
 1. (\<And>W1. \<lbrakk>fst a \<in> I; fst b \<in> I; snd a \<in> \<FF> (fst a); snd b \<in> \<FF> (fst b); W1 \<in> I; W1 \<subseteq> fst a; W1 \<subseteq> fst b; \<rho> (fst a) W1 (snd a) = \<rho> (fst b) W1 (snd b)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst a \<in> I
fst b \<in> I
snd a \<in> \<FF> (fst a)
snd b \<in> \<FF> (fst b)
W1 \<in> I
W1 \<subseteq> fst a
W1 \<subseteq> fst b
\<rho> (fst a) W1 (snd a) = \<rho> (fst b) W1 (snd b)

goal (1 subgoal):
 1. (a, c) \<in> {(x, y). x \<sim> y}
[PROOF STEP]
obtain W2 where W2:"fst b \<in> I" "fst c \<in> I" "snd b \<in> \<FF> (fst b)" "snd c \<in> \<FF> (fst c)"
                    "W2 \<in> I" "W2 \<subseteq> fst b" "W2 \<subseteq> fst c"
                    "\<rho> (fst b) W2 (snd b) = \<rho> (fst c) W2 (snd c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>W2. \<lbrakk>fst b \<in> I; fst c \<in> I; snd b \<in> \<FF> (fst b); snd c \<in> \<FF> (fst c); W2 \<in> I; W2 \<subseteq> fst b; W2 \<subseteq> fst c; \<rho> (fst b) W2 (snd b) = \<rho> (fst c) W2 (snd c)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>(b, c) \<in> {(x, y). x \<sim> y}\<close>
[PROOF STATE]
proof (prove)
using this:
(b, c) \<in> {(x, y). x \<sim> y}

goal (1 subgoal):
 1. (\<And>W2. \<lbrakk>fst b \<in> I; fst c \<in> I; snd b \<in> \<FF> (fst b); snd c \<in> \<FF> (fst c); W2 \<in> I; W2 \<subseteq> fst b; W2 \<subseteq> fst c; \<rho> (fst b) W2 (snd b) = \<rho> (fst c) W2 (snd c)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding rel_def
[PROOF STATE]
proof (prove)
using this:
(b, c) \<in> {(x, y). (fst x \<in> I \<and> fst y \<in> I) \<and> (snd x \<in> \<FF> (fst x) \<and> snd y \<in> \<FF> (fst y)) \<and> (\<exists>W. W \<in> I \<and> W \<subseteq> fst x \<inter> fst y \<and> \<rho> (fst x) W (snd x) = \<rho> (fst y) W (snd y))}

goal (1 subgoal):
 1. (\<And>W2. \<lbrakk>fst b \<in> I; fst c \<in> I; snd b \<in> \<FF> (fst b); snd c \<in> \<FF> (fst c); W2 \<in> I; W2 \<subseteq> fst b; W2 \<subseteq> fst c; \<rho> (fst b) W2 (snd b) = \<rho> (fst c) W2 (snd c)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst b \<in> I
fst c \<in> I
snd b \<in> \<FF> (fst b)
snd c \<in> \<FF> (fst c)
W2 \<in> I
W2 \<subseteq> fst b
W2 \<subseteq> fst c
\<rho> (fst b) W2 (snd b) = \<rho> (fst c) W2 (snd c)

goal (1 subgoal):
 1. (a, c) \<in> {(x, y). x \<sim> y}
[PROOF STEP]
obtain W3 where W3:"W3 \<in>I" "W3 \<subseteq> W1 \<inter> W2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>W3. \<lbrakk>W3 \<in> I; W3 \<subseteq> W1 \<inter> W2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using has_lower_bound[OF \<open>W1\<in>I\<close> \<open>W2\<in>I\<close>]
[PROOF STATE]
proof (prove)
using this:
\<exists>W\<in>I. W \<subseteq> W1 \<inter> W2

goal (1 subgoal):
 1. (\<And>W3. \<lbrakk>W3 \<in> I; W3 \<subseteq> W1 \<inter> W2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
W3 \<in> I
W3 \<subseteq> W1 \<inter> W2

goal (1 subgoal):
 1. (a, c) \<in> {(x, y). x \<sim> y}
[PROOF STEP]
from \<open>W3 \<subseteq> W1 \<inter> W2\<close>
[PROOF STATE]
proof (chain)
picking this:
W3 \<subseteq> W1 \<inter> W2
[PROOF STEP]
have "W3 \<subseteq> fst a \<inter> fst c"
[PROOF STATE]
proof (prove)
using this:
W3 \<subseteq> W1 \<inter> W2

goal (1 subgoal):
 1. W3 \<subseteq> fst a \<inter> fst c
[PROOF STEP]
using W1(6) W2(7)
[PROOF STATE]
proof (prove)
using this:
W3 \<subseteq> W1 \<inter> W2
W1 \<subseteq> fst a
W2 \<subseteq> fst c

goal (1 subgoal):
 1. W3 \<subseteq> fst a \<inter> fst c
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
W3 \<subseteq> fst a \<inter> fst c

goal (1 subgoal):
 1. (a, c) \<in> {(x, y). x \<sim> y}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
W3 \<subseteq> fst a \<inter> fst c

goal (1 subgoal):
 1. (a, c) \<in> {(x, y). x \<sim> y}
[PROOF STEP]
have "\<rho> (fst a) W3 (snd a) = \<rho> (fst c) W3 (snd c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> (fst a) W3 (snd a) = \<rho> (fst c) W3 (snd c)
[PROOF STEP]
using W1 W2
[PROOF STATE]
proof (prove)
using this:
fst a \<in> I
fst b \<in> I
snd a \<in> \<FF> (fst a)
snd b \<in> \<FF> (fst b)
W1 \<in> I
W1 \<subseteq> fst a
W1 \<subseteq> fst b
\<rho> (fst a) W1 (snd a) = \<rho> (fst b) W1 (snd b)
fst b \<in> I
fst c \<in> I
snd b \<in> \<FF> (fst b)
snd c \<in> \<FF> (fst c)
W2 \<in> I
W2 \<subseteq> fst b
W2 \<subseteq> fst c
\<rho> (fst b) W2 (snd b) = \<rho> (fst c) W2 (snd c)

goal (1 subgoal):
 1. \<rho> (fst a) W3 (snd a) = \<rho> (fst c) W3 (snd c)
[PROOF STEP]
by (metis W3(1) W3(2) eq_\<rho> le_inf_iff subset_of_opens)
[PROOF STATE]
proof (state)
this:
\<rho> (fst a) W3 (snd a) = \<rho> (fst c) W3 (snd c)

goal (1 subgoal):
 1. (a, c) \<in> {(x, y). x \<sim> y}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<rho> (fst a) W3 (snd a) = \<rho> (fst c) W3 (snd c)

goal (1 subgoal):
 1. (a, c) \<in> {(x, y). x \<sim> y}
[PROOF STEP]
note \<open>W3 \<in>I\<close> W1 W2
[PROOF STATE]
proof (state)
this:
W3 \<in> I
fst a \<in> I
fst b \<in> I
snd a \<in> \<FF> (fst a)
snd b \<in> \<FF> (fst b)
W1 \<in> I
W1 \<subseteq> fst a
W1 \<subseteq> fst b
\<rho> (fst a) W1 (snd a) = \<rho> (fst b) W1 (snd b)
fst b \<in> I
fst c \<in> I
snd b \<in> \<FF> (fst b)
snd c \<in> \<FF> (fst c)
W2 \<in> I
W2 \<subseteq> fst b
W2 \<subseteq> fst c
\<rho> (fst b) W2 (snd b) = \<rho> (fst c) W2 (snd c)

goal (1 subgoal):
 1. (a, c) \<in> {(x, y). x \<sim> y}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
W3 \<subseteq> fst a \<inter> fst c
\<rho> (fst a) W3 (snd a) = \<rho> (fst c) W3 (snd c)
W3 \<in> I
fst a \<in> I
fst b \<in> I
snd a \<in> \<FF> (fst a)
snd b \<in> \<FF> (fst b)
W1 \<in> I
W1 \<subseteq> fst a
W1 \<subseteq> fst b
\<rho> (fst a) W1 (snd a) = \<rho> (fst b) W1 (snd b)
fst b \<in> I
fst c \<in> I
snd b \<in> \<FF> (fst b)
snd c \<in> \<FF> (fst c)
W2 \<in> I
W2 \<subseteq> fst b
W2 \<subseteq> fst c
\<rho> (fst b) W2 (snd b) = \<rho> (fst c) W2 (snd c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
W3 \<subseteq> fst a \<inter> fst c
\<rho> (fst a) W3 (snd a) = \<rho> (fst c) W3 (snd c)
W3 \<in> I
fst a \<in> I
fst b \<in> I
snd a \<in> \<FF> (fst a)
snd b \<in> \<FF> (fst b)
W1 \<in> I
W1 \<subseteq> fst a
W1 \<subseteq> fst b
\<rho> (fst a) W1 (snd a) = \<rho> (fst b) W1 (snd b)
fst b \<in> I
fst c \<in> I
snd b \<in> \<FF> (fst b)
snd c \<in> \<FF> (fst c)
W2 \<in> I
W2 \<subseteq> fst b
W2 \<subseteq> fst c
\<rho> (fst b) W2 (snd b) = \<rho> (fst c) W2 (snd c)

goal (1 subgoal):
 1. (a, c) \<in> {(x, y). x \<sim> y}
[PROOF STEP]
unfolding rel_def
[PROOF STATE]
proof (prove)
using this:
W3 \<subseteq> fst a \<inter> fst c
\<rho> (fst a) W3 (snd a) = \<rho> (fst c) W3 (snd c)
W3 \<in> I
fst a \<in> I
fst b \<in> I
snd a \<in> \<FF> (fst a)
snd b \<in> \<FF> (fst b)
W1 \<in> I
W1 \<subseteq> fst a
W1 \<subseteq> fst b
\<rho> (fst a) W1 (snd a) = \<rho> (fst b) W1 (snd b)
fst b \<in> I
fst c \<in> I
snd b \<in> \<FF> (fst b)
snd c \<in> \<FF> (fst c)
W2 \<in> I
W2 \<subseteq> fst b
W2 \<subseteq> fst c
\<rho> (fst b) W2 (snd b) = \<rho> (fst c) W2 (snd c)

goal (1 subgoal):
 1. (a, c) \<in> {(x, y). (fst x \<in> I \<and> fst y \<in> I) \<and> (snd x \<in> \<FF> (fst x) \<and> snd y \<in> \<FF> (fst y)) \<and> (\<exists>W. W \<in> I \<and> W \<subseteq> fst x \<inter> fst y \<and> \<rho> (fst x) W (snd x) = \<rho> (fst y) W (snd y))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a, c) \<in> {(x, y). x \<sim> y}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?a1, ?b1) \<in> {(x, y). x \<sim> y}; (?b1, ?c1) \<in> {(x, y). x \<sim> y}\<rbrakk> \<Longrightarrow> (?a1, ?c1) \<in> {(x, y). x \<sim> y}

goal (3 subgoals):
 1. {(x, y). x \<sim> y} \<subseteq> Sigma I \<FF> \<times> Sigma I \<FF>
 2. \<And>a. a \<in> Sigma I \<FF> \<Longrightarrow> (a, a) \<in> {(x, y). x \<sim> y}
 3. \<And>a b. (a, b) \<in> {(x, y). x \<sim> y} \<Longrightarrow> (b, a) \<in> {(x, y). x \<sim> y}
[PROOF STEP]
qed (auto simp: rel_def Int_commute)


[STATEMENT]
lemma class_of_eqD:
  assumes "\<lfloor>U1,s1\<rfloor> = \<lfloor>U2,s2\<rfloor>" "(U1,s1) \<in> Sigma I \<FF>" "(U2,s2) \<in> Sigma I \<FF>"
  obtains W where "W \<in> I" "W \<subseteq> U1 \<inter> U2" "\<rho> U1 W s1 = \<rho> U2 W s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>W. \<lbrakk>W \<in> I; W \<subseteq> U1 \<inter> U2; \<rho> U1 W s1 = \<rho> U2 W s2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using rel.Class_equivalence[OF assms(2,3)] assms(1)
[PROOF STATE]
proof (prove)
using this:
(rel.Class (U1, s1) = rel.Class (U2, s2)) = (((U1, s1), U2, s2) \<in> {(x, y). x \<sim> y})
\<lfloor>U1, s1\<rfloor> = \<lfloor>U2, s2\<rfloor>

goal (1 subgoal):
 1. (\<And>W. \<lbrakk>W \<in> I; W \<subseteq> U1 \<inter> U2; \<rho> U1 W s1 = \<rho> U2 W s2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding class_of_def rel_def
[PROOF STATE]
proof (prove)
using this:
(equivalence.Class (Sigma I \<FF>) {(x, y). (fst x \<in> I \<and> fst y \<in> I) \<and> (snd x \<in> \<FF> (fst x) \<and> snd y \<in> \<FF> (fst y)) \<and> (\<exists>W. W \<in> I \<and> W \<subseteq> fst x \<inter> fst y \<and> \<rho> (fst x) W (snd x) = \<rho> (fst y) W (snd y))} (U1, s1) = equivalence.Class (Sigma I \<FF>) {(x, y). (fst x \<in> I \<and> fst y \<in> I) \<and> (snd x \<in> \<FF> (fst x) \<and> snd y \<in> \<FF> (fst y)) \<and> (\<exists>W. W \<in> I \<and> W \<subseteq> fst x \<inter> fst y \<and> \<rho> (fst x) W (snd x) = \<rho> (fst y) W (snd y))} (U2, s2)) = (((U1, s1), U2, s2) \<in> {(x, y). (fst x \<in> I \<and> fst y \<in> I) \<and> (snd x \<in> \<FF> (fst x) \<and> snd y \<in> \<FF> (fst y)) \<and> (\<exists>W. W \<in> I \<and> W \<subseteq> fst x \<inter> fst y \<and> \<rho> (fst x) W (snd x) = \<rho> (fst y) W (snd y))})
equivalence.Class (Sigma I \<FF>) {(x, y). (fst x \<in> I \<and> fst y \<in> I) \<and> (snd x \<in> \<FF> (fst x) \<and> snd y \<in> \<FF> (fst y)) \<and> (\<exists>W. W \<in> I \<and> W \<subseteq> fst x \<inter> fst y \<and> \<rho> (fst x) W (snd x) = \<rho> (fst y) W (snd y))} (U1, s1) = equivalence.Class (Sigma I \<FF>) {(x, y). (fst x \<in> I \<and> fst y \<in> I) \<and> (snd x \<in> \<FF> (fst x) \<and> snd y \<in> \<FF> (fst y)) \<and> (\<exists>W. W \<in> I \<and> W \<subseteq> fst x \<inter> fst y \<and> \<rho> (fst x) W (snd x) = \<rho> (fst y) W (snd y))} (U2, s2)

goal (1 subgoal):
 1. (\<And>W. \<lbrakk>W \<in> I; W \<subseteq> U1 \<inter> U2; \<rho> U1 W s1 = \<rho> U2 W s2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma class_of_eqI:
  assumes "(U1,s1) \<in> Sigma I \<FF>" "(U2,s2) \<in> Sigma I \<FF>"
  assumes "W \<in> I" "W \<subseteq> U1 \<inter> U2" "\<rho> U1 W s1 = \<rho> U2 W s2"
  shows "\<lfloor>U1,s1\<rfloor> = \<lfloor>U2,s2\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>U1, s1\<rfloor> = \<lfloor>U2, s2\<rfloor>
[PROOF STEP]
unfolding class_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel.Class (U1, s1) = rel.Class (U2, s2)
[PROOF STEP]
apply (rule rel.Class_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((U1, s1), U2, s2) \<in> {(x, y). x \<sim> y}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(U1, s1) \<in> Sigma I \<FF>
(U2, s2) \<in> Sigma I \<FF>
W \<in> I
W \<subseteq> U1 \<inter> U2
\<rho> U1 W s1 = \<rho> U2 W s2

goal (1 subgoal):
 1. ((U1, s1), U2, s2) \<in> {(x, y). x \<sim> y}
[PROOF STEP]
by (auto simp: rel_def)


[STATEMENT]
lemma class_of_0_in:
  assumes "U \<in> I"
  shows "\<zero>\<^bsub>U\<^esub> \<in> \<FF> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero>\<^bsub>U\<^esub> \<in> \<FF> U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<zero>\<^bsub>U\<^esub> \<in> \<FF> U
[PROOF STEP]
have "ring (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
using assms subset_of_opens is_ring_from_is_homomorphism
[PROOF STATE]
proof (prove)
using this:
U \<in> I
?U \<in> I \<Longrightarrow> is_open ?U
is_open ?U \<Longrightarrow> ring (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub>

goal (1 subgoal):
 1. ring (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ring (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>

goal (1 subgoal):
 1. \<zero>\<^bsub>U\<^esub> \<in> \<FF> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ring (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ring (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>

goal (1 subgoal):
 1. \<zero>\<^bsub>U\<^esub> \<in> \<FF> U
[PROOF STEP]
unfolding ring_def abelian_group_def Group_Theory.group_def
[PROOF STATE]
proof (prove)
using this:
((Group_Theory.monoid (\<FF> U) +\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<and> Group_Theory.group_axioms (\<FF> U) +\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub>) \<and> commutative_monoid (\<FF> U) +\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub>) \<and> Group_Theory.monoid (\<FF> U) \<cdot>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> \<and> ring_axioms (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub>

goal (1 subgoal):
 1. \<zero>\<^bsub>U\<^esub> \<in> \<FF> U
[PROOF STEP]
by (meson monoid.unit_closed)
[PROOF STATE]
proof (state)
this:
\<zero>\<^bsub>U\<^esub> \<in> \<FF> U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_Class_iff: "x \<sim> y \<longleftrightarrow> y \<in> Sigma I \<FF> \<and> x \<in> rel.Class y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sim> y = (y \<in> Sigma I \<FF> \<and> x \<in> rel.Class y)
[PROOF STEP]
by blast


[STATEMENT]
lemma class_of_0_eq:
  assumes "U \<in> I" "U' \<in> I"
  shows "\<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<zero>\<^bsub>U'\<^esub>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<zero>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<zero>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
obtain W where W: "W \<in> I" "W \<subseteq> U" "W \<subseteq> U'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>W. \<lbrakk>W \<in> I; W \<subseteq> U; W \<subseteq> U'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Int_subset_iff assms has_lower_bound)
[PROOF STATE]
proof (state)
this:
W \<in> I
W \<subseteq> U
W \<subseteq> U'

goal (1 subgoal):
 1. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<zero>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
W \<in> I
W \<subseteq> U
W \<subseteq> U'
[PROOF STEP]
have "is_open W" "is_open U" "is_open U'"
[PROOF STATE]
proof (prove)
using this:
W \<in> I
W \<subseteq> U
W \<subseteq> U'

goal (1 subgoal):
 1. is_open W &&& is_open U &&& is_open U'
[PROOF STEP]
by (auto simp add: assms subset_of_opens)
[PROOF STATE]
proof (state)
this:
is_open W
is_open U
is_open U'

goal (1 subgoal):
 1. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<zero>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_open W
is_open U
is_open U'
[PROOF STEP]
have "\<rho> U W \<zero>\<^bsub>U\<^esub> = \<rho> U' W \<zero>\<^bsub>U'\<^esub>"
[PROOF STATE]
proof (prove)
using this:
is_open W
is_open U
is_open U'

goal (1 subgoal):
 1. \<rho> U W \<zero>\<^bsub>U\<^esub> = \<rho> U' W \<zero>\<^bsub>U'\<^esub>
[PROOF STEP]
using W is_ring_morphism [of U W] is_ring_morphism [of U' W]
[PROOF STATE]
proof (prove)
using this:
is_open W
is_open U
is_open U'
W \<in> I
W \<subseteq> U
W \<subseteq> U'
\<lbrakk>is_open U; is_open W; W \<subseteq> U\<rbrakk> \<Longrightarrow> ring_homomorphism (\<rho> U W) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> W) +\<^bsub>W\<^esub> \<cdot>\<^bsub>W\<^esub> \<zero>\<^bsub>W\<^esub> \<one>\<^bsub>W\<^esub>
\<lbrakk>is_open U'; is_open W; W \<subseteq> U'\<rbrakk> \<Longrightarrow> ring_homomorphism (\<rho> U' W) (\<FF> U') +\<^bsub>U'\<^esub> \<cdot>\<^bsub>U'\<^esub> \<zero>\<^bsub>U'\<^esub> \<one>\<^bsub>U'\<^esub> (\<FF> W) +\<^bsub>W\<^esub> \<cdot>\<^bsub>W\<^esub> \<zero>\<^bsub>W\<^esub> \<one>\<^bsub>W\<^esub>

goal (1 subgoal):
 1. \<rho> U W \<zero>\<^bsub>U\<^esub> = \<rho> U' W \<zero>\<^bsub>U'\<^esub>
[PROOF STEP]
by (simp add: ring_homomorphism_def group_homomorphism_def monoid_homomorphism_def
               monoid_homomorphism_axioms_def)
[PROOF STATE]
proof (state)
this:
\<rho> U W \<zero>\<^bsub>U\<^esub> = \<rho> U' W \<zero>\<^bsub>U'\<^esub>

goal (1 subgoal):
 1. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<zero>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
with W
[PROOF STATE]
proof (chain)
picking this:
W \<in> I
W \<subseteq> U
W \<subseteq> U'
\<rho> U W \<zero>\<^bsub>U\<^esub> = \<rho> U' W \<zero>\<^bsub>U'\<^esub>
[PROOF STEP]
have "\<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> U' \<and> \<rho> U W \<zero>\<^bsub>U\<^esub> = \<rho> U' W \<zero>\<^bsub>U'\<^esub>"
[PROOF STATE]
proof (prove)
using this:
W \<in> I
W \<subseteq> U
W \<subseteq> U'
\<rho> U W \<zero>\<^bsub>U\<^esub> = \<rho> U' W \<zero>\<^bsub>U'\<^esub>

goal (1 subgoal):
 1. \<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> U' \<and> \<rho> U W \<zero>\<^bsub>U\<^esub> = \<rho> U' W \<zero>\<^bsub>U'\<^esub>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> U' \<and> \<rho> U W \<zero>\<^bsub>U\<^esub> = \<rho> U' W \<zero>\<^bsub>U'\<^esub>

goal (1 subgoal):
 1. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<zero>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> U' \<and> \<rho> U W \<zero>\<^bsub>U\<^esub> = \<rho> U' W \<zero>\<^bsub>U'\<^esub>

goal (1 subgoal):
 1. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<zero>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
have "\<zero>\<^bsub>U\<^esub> \<in> \<FF> U" "\<zero>\<^bsub>U'\<^esub> \<in> \<FF> U'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero>\<^bsub>U\<^esub> \<in> \<FF> U &&& \<zero>\<^bsub>U'\<^esub> \<in> \<FF> U'
[PROOF STEP]
by (auto simp add: assms class_of_0_in)
[PROOF STATE]
proof (state)
this:
\<zero>\<^bsub>U\<^esub> \<in> \<FF> U
\<zero>\<^bsub>U'\<^esub> \<in> \<FF> U'

goal (1 subgoal):
 1. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<zero>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> U' \<and> \<rho> U W \<zero>\<^bsub>U\<^esub> = \<rho> U' W \<zero>\<^bsub>U'\<^esub>
\<zero>\<^bsub>U\<^esub> \<in> \<FF> U
\<zero>\<^bsub>U'\<^esub> \<in> \<FF> U'
[PROOF STEP]
have "(U, \<zero>\<^bsub>U\<^esub>) \<sim> (U', \<zero>\<^bsub>U'\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> U' \<and> \<rho> U W \<zero>\<^bsub>U\<^esub> = \<rho> U' W \<zero>\<^bsub>U'\<^esub>
\<zero>\<^bsub>U\<^esub> \<in> \<FF> U
\<zero>\<^bsub>U'\<^esub> \<in> \<FF> U'

goal (1 subgoal):
 1. (U, \<zero>\<^bsub>U\<^esub>) \<sim> (U', \<zero>\<^bsub>U'\<^esub>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> U' \<and> \<rho> U W \<zero>\<^bsub>U\<^esub> = \<rho> U' W \<zero>\<^bsub>U'\<^esub>
\<zero>\<^bsub>U\<^esub> \<in> \<FF> U
\<zero>\<^bsub>U'\<^esub> \<in> \<FF> U'
U \<in> I
U' \<in> I

goal (1 subgoal):
 1. (U, \<zero>\<^bsub>U\<^esub>) \<sim> (U', \<zero>\<^bsub>U'\<^esub>)
[PROOF STEP]
by (auto simp: rel_def)
[PROOF STATE]
proof (state)
this:
(U, \<zero>\<^bsub>U\<^esub>) \<sim> (U', \<zero>\<^bsub>U'\<^esub>)

goal (1 subgoal):
 1. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<zero>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(U, \<zero>\<^bsub>U\<^esub>) \<sim> (U', \<zero>\<^bsub>U'\<^esub>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(U, \<zero>\<^bsub>U\<^esub>) \<sim> (U', \<zero>\<^bsub>U'\<^esub>)

goal (1 subgoal):
 1. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<zero>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
unfolding class_of_def
[PROOF STATE]
proof (prove)
using this:
(U, \<zero>\<^bsub>U\<^esub>) \<sim> (U', \<zero>\<^bsub>U'\<^esub>)

goal (1 subgoal):
 1. rel.Class (U, \<zero>\<^bsub>U\<^esub>) = rel.Class (U', \<zero>\<^bsub>U'\<^esub>)
[PROOF STEP]
by (simp add: rel.Class_eq)
[PROOF STATE]
proof (state)
this:
\<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<zero>\<^bsub>U'\<^esub>\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma class_of_1_in:
  assumes "U \<in> I"
  shows "\<one>\<^bsub>U\<^esub> \<in> \<FF> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one>\<^bsub>U\<^esub> \<in> \<FF> U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<one>\<^bsub>U\<^esub> \<in> \<FF> U
[PROOF STEP]
have "ring (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
using assms subset_of_opens is_ring_from_is_homomorphism
[PROOF STATE]
proof (prove)
using this:
U \<in> I
?U \<in> I \<Longrightarrow> is_open ?U
is_open ?U \<Longrightarrow> ring (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub>

goal (1 subgoal):
 1. ring (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ring (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>

goal (1 subgoal):
 1. \<one>\<^bsub>U\<^esub> \<in> \<FF> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ring (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ring (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>

goal (1 subgoal):
 1. \<one>\<^bsub>U\<^esub> \<in> \<FF> U
[PROOF STEP]
unfolding ring_def
[PROOF STATE]
proof (prove)
using this:
abelian_group (\<FF> U) +\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<and> Group_Theory.monoid (\<FF> U) \<cdot>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> \<and> ring_axioms (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub>

goal (1 subgoal):
 1. \<one>\<^bsub>U\<^esub> \<in> \<FF> U
[PROOF STEP]
by (meson monoid.unit_closed)
[PROOF STATE]
proof (state)
this:
\<one>\<^bsub>U\<^esub> \<in> \<FF> U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma class_of_1_eq:
  assumes "U \<in> I" and "U' \<in> I"
  shows "\<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<one>\<^bsub>U'\<^esub>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<one>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<one>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
obtain W where W: "W \<in> I" "W \<subseteq> U" "W \<subseteq> U'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>W. \<lbrakk>W \<in> I; W \<subseteq> U; W \<subseteq> U'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Int_subset_iff assms has_lower_bound)
[PROOF STATE]
proof (state)
this:
W \<in> I
W \<subseteq> U
W \<subseteq> U'

goal (1 subgoal):
 1. \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<one>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
W \<in> I
W \<subseteq> U
W \<subseteq> U'
[PROOF STEP]
have "is_open W" "is_open U" "is_open U'"
[PROOF STATE]
proof (prove)
using this:
W \<in> I
W \<subseteq> U
W \<subseteq> U'

goal (1 subgoal):
 1. is_open W &&& is_open U &&& is_open U'
[PROOF STEP]
by (auto simp add: assms subset_of_opens)
[PROOF STATE]
proof (state)
this:
is_open W
is_open U
is_open U'

goal (1 subgoal):
 1. \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<one>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_open W
is_open U
is_open U'
[PROOF STEP]
have "\<rho> U W \<one>\<^bsub>U\<^esub> = \<rho> U' W \<one>\<^bsub>U'\<^esub>"
[PROOF STATE]
proof (prove)
using this:
is_open W
is_open U
is_open U'

goal (1 subgoal):
 1. \<rho> U W \<one>\<^bsub>U\<^esub> = \<rho> U' W \<one>\<^bsub>U'\<^esub>
[PROOF STEP]
using W is_ring_morphism [of U W] is_ring_morphism [of U' W]
[PROOF STATE]
proof (prove)
using this:
is_open W
is_open U
is_open U'
W \<in> I
W \<subseteq> U
W \<subseteq> U'
\<lbrakk>is_open U; is_open W; W \<subseteq> U\<rbrakk> \<Longrightarrow> ring_homomorphism (\<rho> U W) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> W) +\<^bsub>W\<^esub> \<cdot>\<^bsub>W\<^esub> \<zero>\<^bsub>W\<^esub> \<one>\<^bsub>W\<^esub>
\<lbrakk>is_open U'; is_open W; W \<subseteq> U'\<rbrakk> \<Longrightarrow> ring_homomorphism (\<rho> U' W) (\<FF> U') +\<^bsub>U'\<^esub> \<cdot>\<^bsub>U'\<^esub> \<zero>\<^bsub>U'\<^esub> \<one>\<^bsub>U'\<^esub> (\<FF> W) +\<^bsub>W\<^esub> \<cdot>\<^bsub>W\<^esub> \<zero>\<^bsub>W\<^esub> \<one>\<^bsub>W\<^esub>

goal (1 subgoal):
 1. \<rho> U W \<one>\<^bsub>U\<^esub> = \<rho> U' W \<one>\<^bsub>U'\<^esub>
[PROOF STEP]
by (simp add: ring_homomorphism_def group_homomorphism_def monoid_homomorphism_def
               monoid_homomorphism_axioms_def)
[PROOF STATE]
proof (state)
this:
\<rho> U W \<one>\<^bsub>U\<^esub> = \<rho> U' W \<one>\<^bsub>U'\<^esub>

goal (1 subgoal):
 1. \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<one>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
with W
[PROOF STATE]
proof (chain)
picking this:
W \<in> I
W \<subseteq> U
W \<subseteq> U'
\<rho> U W \<one>\<^bsub>U\<^esub> = \<rho> U' W \<one>\<^bsub>U'\<^esub>
[PROOF STEP]
have "\<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> U' \<and> \<rho> U W \<one>\<^bsub>U\<^esub> = \<rho> U' W \<one>\<^bsub>U'\<^esub>"
[PROOF STATE]
proof (prove)
using this:
W \<in> I
W \<subseteq> U
W \<subseteq> U'
\<rho> U W \<one>\<^bsub>U\<^esub> = \<rho> U' W \<one>\<^bsub>U'\<^esub>

goal (1 subgoal):
 1. \<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> U' \<and> \<rho> U W \<one>\<^bsub>U\<^esub> = \<rho> U' W \<one>\<^bsub>U'\<^esub>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> U' \<and> \<rho> U W \<one>\<^bsub>U\<^esub> = \<rho> U' W \<one>\<^bsub>U'\<^esub>

goal (1 subgoal):
 1. \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<one>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> U' \<and> \<rho> U W \<one>\<^bsub>U\<^esub> = \<rho> U' W \<one>\<^bsub>U'\<^esub>

goal (1 subgoal):
 1. \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<one>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
have "\<one>\<^bsub>U\<^esub> \<in> \<FF> U" "\<one>\<^bsub>U'\<^esub> \<in> \<FF> U'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one>\<^bsub>U\<^esub> \<in> \<FF> U &&& \<one>\<^bsub>U'\<^esub> \<in> \<FF> U'
[PROOF STEP]
by (auto simp add: assms class_of_1_in)
[PROOF STATE]
proof (state)
this:
\<one>\<^bsub>U\<^esub> \<in> \<FF> U
\<one>\<^bsub>U'\<^esub> \<in> \<FF> U'

goal (1 subgoal):
 1. \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<one>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> U' \<and> \<rho> U W \<one>\<^bsub>U\<^esub> = \<rho> U' W \<one>\<^bsub>U'\<^esub>
\<one>\<^bsub>U\<^esub> \<in> \<FF> U
\<one>\<^bsub>U'\<^esub> \<in> \<FF> U'
[PROOF STEP]
have "(U, \<one>\<^bsub>U\<^esub>) \<sim> (U', \<one>\<^bsub>U'\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> U' \<and> \<rho> U W \<one>\<^bsub>U\<^esub> = \<rho> U' W \<one>\<^bsub>U'\<^esub>
\<one>\<^bsub>U\<^esub> \<in> \<FF> U
\<one>\<^bsub>U'\<^esub> \<in> \<FF> U'

goal (1 subgoal):
 1. (U, \<one>\<^bsub>U\<^esub>) \<sim> (U', \<one>\<^bsub>U'\<^esub>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<exists>W. W \<in> I \<and> W \<subseteq> U \<and> W \<subseteq> U' \<and> \<rho> U W \<one>\<^bsub>U\<^esub> = \<rho> U' W \<one>\<^bsub>U'\<^esub>
\<one>\<^bsub>U\<^esub> \<in> \<FF> U
\<one>\<^bsub>U'\<^esub> \<in> \<FF> U'
U \<in> I
U' \<in> I

goal (1 subgoal):
 1. (U, \<one>\<^bsub>U\<^esub>) \<sim> (U', \<one>\<^bsub>U'\<^esub>)
[PROOF STEP]
by (auto simp: rel_def)
[PROOF STATE]
proof (state)
this:
(U, \<one>\<^bsub>U\<^esub>) \<sim> (U', \<one>\<^bsub>U'\<^esub>)

goal (1 subgoal):
 1. \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<one>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(U, \<one>\<^bsub>U\<^esub>) \<sim> (U', \<one>\<^bsub>U'\<^esub>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(U, \<one>\<^bsub>U\<^esub>) \<sim> (U', \<one>\<^bsub>U'\<^esub>)

goal (1 subgoal):
 1. \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<one>\<^bsub>U'\<^esub>\<rfloor>
[PROOF STEP]
unfolding class_of_def
[PROOF STATE]
proof (prove)
using this:
(U, \<one>\<^bsub>U\<^esub>) \<sim> (U', \<one>\<^bsub>U'\<^esub>)

goal (1 subgoal):
 1. rel.Class (U, \<one>\<^bsub>U\<^esub>) = rel.Class (U', \<one>\<^bsub>U'\<^esub>)
[PROOF STEP]
by (simp add: rel.Class_eq)
[PROOF STATE]
proof (state)
this:
\<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>U', \<one>\<^bsub>U'\<^esub>\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zero_rel_carrier[intro]:
  assumes "U \<in> I"
  shows "\<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim
[PROOF STEP]
unfolding carrier_direct_lim_def class_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel.Class (U, \<zero>\<^bsub>U\<^esub>) \<in> rel.Partition
[PROOF STEP]
proof (rule rel.Block_closed)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (U, \<zero>\<^bsub>U\<^esub>) \<in> Sigma I \<FF>
[PROOF STEP]
interpret ring "(\<FF> U)" "+\<^bsub>U\<^esub>" "\<cdot>\<^bsub>U\<^esub>" "\<zero>\<^bsub>U\<^esub>" "\<one>\<^bsub>U\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub>
[PROOF STEP]
by (simp add: assms is_ring_from_is_homomorphism subset_of_opens)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (U, \<zero>\<^bsub>U\<^esub>) \<in> Sigma I \<FF>
[PROOF STEP]
show "(U, \<zero>\<^bsub>U\<^esub>) \<in> Sigma I \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (U, \<zero>\<^bsub>U\<^esub>) \<in> Sigma I \<FF>
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
(U, \<zero>\<^bsub>U\<^esub>) \<in> Sigma I \<FF>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_rel_carrier[intro]:
  assumes "U \<in> I"
  shows "\<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim
[PROOF STEP]
unfolding carrier_direct_lim_def class_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel.Class (U, \<one>\<^bsub>U\<^esub>) \<in> rel.Partition
[PROOF STEP]
apply (rule rel.Block_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (U, \<one>\<^bsub>U\<^esub>) \<in> Sigma I \<FF>
[PROOF STEP]
by (simp add: assms class_of_1_in)


[STATEMENT]
lemma rel_carrier_Eps_in:
  fixes X :: "('a set \<times> 'b) set"
  defines "a\<equiv>(SOME x. x \<in> X)"
  assumes "X \<in> carrier_direct_lim"
  shows "a \<in> X" "a \<in>Sigma I \<FF>"  "X = \<lfloor>fst a, snd a\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> X &&& a \<in> Sigma I \<FF> &&& X = \<lfloor>fst a, snd a\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. a \<in> X
 2. a \<in> Sigma I \<FF>
 3. X = \<lfloor>fst a, snd a\<rfloor>
[PROOF STEP]
have "\<exists>a\<in>Sigma I \<FF>. a \<in> X \<and> X = rel.Class a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a\<in>Sigma I \<FF>. a \<in> X \<and> X = rel.Class a
[PROOF STEP]
using rel.representant_exists[OF \<open>X \<in> carrier_direct_lim\<close>[unfolded carrier_direct_lim_def]]
[PROOF STATE]
proof (prove)
using this:
\<exists>a\<in>Sigma I \<FF>. a \<in> X \<and> X = rel.Class a

goal (1 subgoal):
 1. \<exists>a\<in>Sigma I \<FF>. a \<in> X \<and> X = rel.Class a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>Sigma I \<FF>. a \<in> X \<and> X = rel.Class a

goal (3 subgoals):
 1. a \<in> X
 2. a \<in> Sigma I \<FF>
 3. X = \<lfloor>fst a, snd a\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a\<in>Sigma I \<FF>. a \<in> X \<and> X = rel.Class a
[PROOF STEP]
have "a \<in> X \<and> a \<in>Sigma I \<FF> \<and> X = \<lfloor>fst a, snd a\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\<exists>a\<in>Sigma I \<FF>. a \<in> X \<and> X = rel.Class a

goal (1 subgoal):
 1. a \<in> X \<and> a \<in> Sigma I \<FF> \<and> X = \<lfloor>fst a, snd a\<rfloor>
[PROOF STEP]
unfolding class_of_def
[PROOF STATE]
proof (prove)
using this:
\<exists>a\<in>Sigma I \<FF>. a \<in> X \<and> X = rel.Class a

goal (1 subgoal):
 1. a \<in> X \<and> a \<in> Sigma I \<FF> \<and> X = rel.Class (fst a, snd a)
[PROOF STEP]
by (metis a_def assms(2) carrier_direct_lim_def ex_in_conv prod.collapse rel.Block_self
        rel.Class_closed some_in_eq)
[PROOF STATE]
proof (state)
this:
a \<in> X \<and> a \<in> Sigma I \<FF> \<and> X = \<lfloor>fst a, snd a\<rfloor>

goal (3 subgoals):
 1. a \<in> X
 2. a \<in> Sigma I \<FF>
 3. X = \<lfloor>fst a, snd a\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> X \<and> a \<in> Sigma I \<FF> \<and> X = \<lfloor>fst a, snd a\<rfloor>
[PROOF STEP]
show "a \<in> X" "a \<in>Sigma I \<FF>"  "X = \<lfloor>fst a, snd a\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
a \<in> X \<and> a \<in> Sigma I \<FF> \<and> X = \<lfloor>fst a, snd a\<rfloor>

goal (1 subgoal):
 1. a \<in> X &&& a \<in> Sigma I \<FF> &&& X = \<lfloor>fst a, snd a\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> X
a \<in> Sigma I \<FF>
X = \<lfloor>fst a, snd a\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_rel_carrier[intro]:
  assumes "X \<in> carrier_direct_lim" "Y \<in> carrier_direct_lim"
  shows "add_rel X Y \<in> carrier_direct_lim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
define x where "x=(SOME x. x \<in> X)"
[PROOF STATE]
proof (state)
this:
x = (SOME x. x \<in> X)

goal (1 subgoal):
 1. add_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
define y where "y=(SOME y. y \<in> Y)"
[PROOF STATE]
proof (state)
this:
y = (SOME y. y \<in> Y)

goal (1 subgoal):
 1. add_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
define z where "z=get_lower_bound (fst x) (fst y)"
[PROOF STATE]
proof (state)
this:
z = get_lower_bound (fst x) (fst y)

goal (1 subgoal):
 1. add_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
have "x\<in>X" "x\<in>Sigma I \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> X &&& x \<in> Sigma I \<FF>
[PROOF STEP]
using rel_carrier_Eps_in[OF \<open>X \<in> carrier_direct_lim\<close>]
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> X) \<in> X
(SOME x. x \<in> X) \<in> Sigma I \<FF>
X = \<lfloor>fst (SOME x. x \<in> X), snd (SOME x. x \<in> X)\<rfloor>

goal (1 subgoal):
 1. x \<in> X &&& x \<in> Sigma I \<FF>
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> X) \<in> X
(SOME x. x \<in> X) \<in> Sigma I \<FF>
X = \<lfloor>fst (SOME x. x \<in> X), snd (SOME x. x \<in> X)\<rfloor>

goal (1 subgoal):
 1. (SOME x. x \<in> X) \<in> X &&& (SOME x. x \<in> X) \<in> Sigma I \<FF>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> X
x \<in> Sigma I \<FF>

goal (1 subgoal):
 1. add_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
have "y\<in>Y" "y \<in> Sigma I \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> Y &&& y \<in> Sigma I \<FF>
[PROOF STEP]
using rel_carrier_Eps_in[OF \<open>Y \<in> carrier_direct_lim\<close>]
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> Y) \<in> Y
(SOME x. x \<in> Y) \<in> Sigma I \<FF>
Y = \<lfloor>fst (SOME x. x \<in> Y), snd (SOME x. x \<in> Y)\<rfloor>

goal (1 subgoal):
 1. y \<in> Y &&& y \<in> Sigma I \<FF>
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> Y) \<in> Y
(SOME x. x \<in> Y) \<in> Sigma I \<FF>
Y = \<lfloor>fst (SOME x. x \<in> Y), snd (SOME x. x \<in> Y)\<rfloor>

goal (1 subgoal):
 1. (SOME y. y \<in> Y) \<in> Y &&& (SOME y. y \<in> Y) \<in> Sigma I \<FF>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> Y
y \<in> Sigma I \<FF>

goal (1 subgoal):
 1. add_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
have "add_rel X Y = \<lfloor>z, add_str z (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel X Y = \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor>
[PROOF STEP]
unfolding add_rel_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>get_lower_bound (fst (SOME x. x \<in> X)) (fst (SOME y. y \<in> Y)), +\<^bsub>get_lower_bound (fst (SOME x. x \<in> X)) (fst (SOME y. y \<in> Y))\<^esub> (\<rho> (fst (SOME x. x \<in> X)) (get_lower_bound (fst (SOME x. x \<in> X)) (fst (SOME y. y \<in> Y))) (snd (SOME x. x \<in> X))) (\<rho> (fst (SOME y. y \<in> Y)) (get_lower_bound (fst (SOME x. x \<in> X)) (fst (SOME y. y \<in> Y))) (snd (SOME y. y \<in> Y)))\<rfloor> = \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor>
[PROOF STEP]
by (fold x_def y_def z_def,rule)
[PROOF STATE]
proof (state)
this:
add_rel X Y = \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor>

goal (1 subgoal):
 1. add_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
add_rel X Y = \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor>

goal (1 subgoal):
 1. add_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
have "... \<in> carrier_direct_lim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> \<in> carrier_direct_lim
[PROOF STEP]
unfolding carrier_direct_lim_def class_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel.Class (z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))) \<in> rel.Partition
[PROOF STEP]
proof (rule rel.Block_closed)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))) \<in> Sigma I \<FF>
[PROOF STEP]
have "z\<in>I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> I
[PROOF STEP]
using \<open>x\<in>Sigma I \<FF>\<close> \<open>y\<in>Sigma I \<FF>\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> Sigma I \<FF>
y \<in> Sigma I \<FF>

goal (1 subgoal):
 1. z \<in> I
[PROOF STEP]
unfolding z_def
[PROOF STATE]
proof (prove)
using this:
x \<in> Sigma I \<FF>
y \<in> Sigma I \<FF>

goal (1 subgoal):
 1. get_lower_bound (fst x) (fst y) \<in> I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> I

goal (1 subgoal):
 1. (z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))) \<in> Sigma I \<FF>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> I
[PROOF STEP]
interpret ring "(\<FF> z)" "+\<^bsub>z\<^esub>" "\<cdot>\<^bsub>z\<^esub>" "\<zero>\<^bsub>z\<^esub>" "\<one>\<^bsub>z\<^esub>"
[PROOF STATE]
proof (prove)
using this:
z \<in> I

goal (1 subgoal):
 1. ring (\<FF> z) +\<^bsub>z\<^esub> \<cdot>\<^bsub>z\<^esub> \<zero>\<^bsub>z\<^esub> \<one>\<^bsub>z\<^esub>
[PROOF STEP]
using is_ring_from_is_homomorphism subset_of_opens
[PROOF STATE]
proof (prove)
using this:
z \<in> I
is_open ?U \<Longrightarrow> ring (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub>
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. ring (\<FF> z) +\<^bsub>z\<^esub> \<cdot>\<^bsub>z\<^esub> \<zero>\<^bsub>z\<^esub> \<one>\<^bsub>z\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))) \<in> Sigma I \<FF>
[PROOF STEP]
show "(z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))) \<in> Sigma I \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))) \<in> Sigma I \<FF>
[PROOF STEP]
using \<open>z\<in>I\<close>
[PROOF STATE]
proof (prove)
using this:
z \<in> I

goal (1 subgoal):
 1. (z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))) \<in> Sigma I \<FF>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> I \<Longrightarrow> +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y)) \<in> \<FF> z
[PROOF STEP]
by (metis \<open>x \<in> Sigma I \<FF>\<close> \<open>y \<in> Sigma I \<FF>\<close> additive.composition_closed
          direct_lim.subset_of_opens direct_lim_axioms get_lower_bound(2) get_lower_bound(3)
          is_map_from_is_homomorphism map.map_closed mem_Sigma_iff prod.exhaust_sel z_def)
[PROOF STATE]
proof (state)
this:
(z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))) \<in> Sigma I \<FF>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> \<in> carrier_direct_lim

goal (1 subgoal):
 1. add_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
add_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
add_rel X Y \<in> carrier_direct_lim

goal (1 subgoal):
 1. add_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
add_rel X Y \<in> carrier_direct_lim

goal:
No subgoals!
[PROOF STEP]
qed