[STATEMENT]
lemma smooth_bump_functionE:
  assumes "closedin (top_of_set carrier) A"
    and "A \<subseteq> U" "U \<subseteq> carrier" "open U"
  obtains \<psi>::"'a \<Rightarrow> real" where
    "diff_fun k charts \<psi>"
    "\<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<psi> x"
    "\<And>x. x \<in> carrier \<Longrightarrow> \<psi> x \<le> 1"
    "\<And>x. x \<in> A \<Longrightarrow> \<psi> x = 1"
    "csupport_on carrier \<psi> \<inter> carrier \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>diff_fun k charts \<psi>; \<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<psi> x; \<And>x. x \<in> carrier \<Longrightarrow> \<psi> x \<le> 1; \<And>x. x \<in> A \<Longrightarrow> \<psi> x = 1; csupport_on carrier \<psi> \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>diff_fun k charts \<psi>; \<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<psi> x; \<And>x. x \<in> carrier \<Longrightarrow> \<psi> x \<le> 1; \<And>x. x \<in> A \<Longrightarrow> \<psi> x = 1; csupport_on carrier \<psi> \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define V where "V x = (if x = 0 then U else carrier - A)" for x::nat
[PROOF STATE]
proof (state)
this:
V ?x = (if ?x = 0 then U else carrier - A)

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>diff_fun k charts \<psi>; \<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<psi> x; \<And>x. x \<in> carrier \<Longrightarrow> \<psi> x \<le> 1; \<And>x. x \<in> A \<Longrightarrow> \<psi> x = 1; csupport_on carrier \<psi> \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "open (carrier - A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (carrier - A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
closedin (top_of_set carrier) A
A \<subseteq> U
U \<subseteq> carrier
open U

goal (1 subgoal):
 1. open (carrier - A)
[PROOF STEP]
by (metis closedin_def open_Int open_carrier openin_open topspace_euclidean_subtopology)
[PROOF STATE]
proof (state)
this:
open (carrier - A)

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>diff_fun k charts \<psi>; \<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<psi> x; \<And>x. x \<in> carrier \<Longrightarrow> \<psi> x \<le> 1; \<And>x. x \<in> A \<Longrightarrow> \<psi> x = 1; csupport_on carrier \<psi> \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open (carrier - A)
[PROOF STEP]
have V: "carrier \<subseteq> (\<Union>i\<in>{0, 1}. V i)" "i \<in> {0, 1} \<Longrightarrow> open (V i)" for i
[PROOF STATE]
proof (prove)
using this:
open (carrier - A)

goal (1 subgoal):
 1. carrier \<subseteq> \<Union> (V ` {0, 1}) &&& (i \<in> {0, 1} \<Longrightarrow> open (V i))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
open (carrier - A)
closedin (top_of_set carrier) A
A \<subseteq> U
U \<subseteq> carrier
open U

goal (1 subgoal):
 1. carrier \<subseteq> \<Union> (V ` {0, 1}) &&& (i \<in> {0, 1} \<Longrightarrow> open (V i))
[PROOF STEP]
by (auto simp: V_def)
[PROOF STATE]
proof (state)
this:
carrier \<subseteq> \<Union> (V ` {0, 1})
?i2 \<in> {0, 1} \<Longrightarrow> open (V ?i2)

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>diff_fun k charts \<psi>; \<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<psi> x; \<And>x. x \<in> carrier \<Longrightarrow> \<psi> x \<le> 1; \<And>x. x \<in> A \<Longrightarrow> \<psi> x = 1; csupport_on carrier \<psi> \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain \<phi>::"nat \<Rightarrow> 'a \<Rightarrow> real" where \<phi>:
    "(\<And>i. i \<in> {0, 1} \<Longrightarrow> diff_fun k charts (\<phi> i))"
    "(\<And>i x. i \<in> {0, 1} \<Longrightarrow> x \<in> carrier \<Longrightarrow> 0 \<le> \<phi> i x)"
    "(\<And>i x. i \<in> {0, 1} \<Longrightarrow> x \<in> carrier \<Longrightarrow> \<phi> i x \<le> 1)"
    "(\<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> {0, 1} \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1)"
    "(\<And>i. i \<in> {0, 1} \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> V i)"
    "locally_finite_on carrier {0, 1} (\<lambda>i. csupport_on carrier (\<phi> i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> {0, 1} \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> {0, 1}; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> {0, 1}; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> {0, 1} \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> {0, 1} \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> V i; locally_finite_on carrier {0, 1} (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule partitions_of_unityE[OF V]) auto
[PROOF STATE]
proof (state)
this:
?i2 \<in> {0, 1} \<Longrightarrow> diff_fun k charts (\<phi> ?i2)
\<lbrakk>?i2 \<in> {0, 1}; ?x2 \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> ?i2 ?x2
\<lbrakk>?i2 \<in> {0, 1}; ?x2 \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> ?i2 ?x2 \<le> 1
?x2 \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> {0, 1} \<and> \<phi> i ?x2 \<noteq> 0. \<phi> i ?x2) = 1
?i2 \<in> {0, 1} \<Longrightarrow> csupport_on carrier (\<phi> ?i2) \<inter> carrier \<subseteq> V ?i2
locally_finite_on carrier {0, 1} (\<lambda>i. csupport_on carrier (\<phi> i))

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>diff_fun k charts \<psi>; \<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<psi> x; \<And>x. x \<in> carrier \<Longrightarrow> \<psi> x \<le> 1; \<And>x. x \<in> A \<Longrightarrow> \<psi> x = 1; csupport_on carrier \<psi> \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from this(1-3,5)[of 0] this(6)
[PROOF STATE]
proof (chain)
picking this:
0 \<in> {0, 1} \<Longrightarrow> diff_fun k charts (\<phi> 0)
\<lbrakk>0 \<in> {0, 1}; ?x2 \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> 0 ?x2
\<lbrakk>0 \<in> {0, 1}; ?x2 \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> 0 ?x2 \<le> 1
0 \<in> {0, 1} \<Longrightarrow> csupport_on carrier (\<phi> 0) \<inter> carrier \<subseteq> V 0
locally_finite_on carrier {0, 1} (\<lambda>i. csupport_on carrier (\<phi> i))
[PROOF STEP]
have "diff_fun k charts (\<phi> 0)"
    "\<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<phi> 0 x"
    "\<And>x. x \<in> carrier \<Longrightarrow> \<phi> 0 x \<le> 1"
    "csupport_on carrier (\<phi> 0) \<inter> carrier \<subseteq> U"
[PROOF STATE]
proof (prove)
using this:
0 \<in> {0, 1} \<Longrightarrow> diff_fun k charts (\<phi> 0)
\<lbrakk>0 \<in> {0, 1}; ?x2 \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> 0 ?x2
\<lbrakk>0 \<in> {0, 1}; ?x2 \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> 0 ?x2 \<le> 1
0 \<in> {0, 1} \<Longrightarrow> csupport_on carrier (\<phi> 0) \<inter> carrier \<subseteq> V 0
locally_finite_on carrier {0, 1} (\<lambda>i. csupport_on carrier (\<phi> i))

goal (1 subgoal):
 1. (diff_fun k charts (\<phi> 0) &&& (\<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<phi> 0 x)) &&& (\<And>x. x \<in> carrier \<Longrightarrow> \<phi> 0 x \<le> 1) &&& csupport_on carrier (\<phi> 0) \<inter> carrier \<subseteq> U
[PROOF STEP]
by (auto simp: V_def)
[PROOF STATE]
proof (state)
this:
diff_fun k charts (\<phi> 0)
?x2 \<in> carrier \<Longrightarrow> 0 \<le> \<phi> 0 ?x2
?x2 \<in> carrier \<Longrightarrow> \<phi> 0 ?x2 \<le> 1
csupport_on carrier (\<phi> 0) \<inter> carrier \<subseteq> U

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>diff_fun k charts \<psi>; \<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<psi> x; \<And>x. x \<in> carrier \<Longrightarrow> \<psi> x \<le> 1; \<And>x. x \<in> A \<Longrightarrow> \<psi> x = 1; csupport_on carrier \<psi> \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
diff_fun k charts (\<phi> 0)
?x2 \<in> carrier \<Longrightarrow> 0 \<le> \<phi> 0 ?x2
?x2 \<in> carrier \<Longrightarrow> \<phi> 0 ?x2 \<le> 1
csupport_on carrier (\<phi> 0) \<inter> carrier \<subseteq> U

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>diff_fun k charts \<psi>; \<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<psi> x; \<And>x. x \<in> carrier \<Longrightarrow> \<psi> x \<le> 1; \<And>x. x \<in> A \<Longrightarrow> \<psi> x = 1; csupport_on carrier \<psi> \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<phi> 0 x = 1" if "x \<in> A" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> 0 x = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> 0 x = 1
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
[PROOF STEP]
have "x \<in> carrier"
[PROOF STATE]
proof (prove)
using this:
x \<in> A

goal (1 subgoal):
 1. x \<in> carrier
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> A
closedin (top_of_set carrier) A
A \<subseteq> U
U \<subseteq> carrier
open U

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

goal (1 subgoal):
 1. \<phi> 0 x = 1
[PROOF STEP]
from \<phi>(4)[OF this]
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i | i \<in> {0, 1} \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1
[PROOF STEP]
have "1 = (\<Sum>i | i \<in> {0, 1} \<and> \<phi> i x \<noteq> 0. \<phi> i x)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i | i \<in> {0, 1} \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1

goal (1 subgoal):
 1. 1 = (\<Sum>i | i \<in> {0, 1} \<and> \<phi> i x \<noteq> 0. \<phi> i x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 = (\<Sum>i | i \<in> {0, 1} \<and> \<phi> i x \<noteq> 0. \<phi> i x)

goal (1 subgoal):
 1. \<phi> 0 x = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 = (\<Sum>i | i \<in> {0, 1} \<and> \<phi> i x \<noteq> 0. \<phi> i x)

goal (1 subgoal):
 1. \<phi> 0 x = 1
[PROOF STEP]
have "{i. i \<in> {0, 1} \<and> \<phi> i x \<noteq> 0} =
      (if \<phi> 0 x \<noteq> 0 then {0} else {}) \<union> (if \<phi> 1 x \<noteq> 0 then {1} else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i \<in> {0, 1}. \<phi> i x \<noteq> 0} = (if \<phi> 0 x \<noteq> 0 then {0} else {}) \<union> (if \<phi> 1 x \<noteq> 0 then {1} else {})
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<phi> 0 x = 0; \<phi> (Suc 0) x = 0; \<phi> xa x \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < xa
[PROOF STEP]
using neq0_conv
[PROOF STATE]
proof (prove)
using this:
(?n \<noteq> 0) = (0 < ?n)

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<phi> 0 x = 0; \<phi> (Suc 0) x = 0; \<phi> xa x \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < xa
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{i \<in> {0, 1}. \<phi> i x \<noteq> 0} = (if \<phi> 0 x \<noteq> 0 then {0} else {}) \<union> (if \<phi> 1 x \<noteq> 0 then {1} else {})

goal (1 subgoal):
 1. \<phi> 0 x = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{i \<in> {0, 1}. \<phi> i x \<noteq> 0} = (if \<phi> 0 x \<noteq> 0 then {0} else {}) \<union> (if \<phi> 1 x \<noteq> 0 then {1} else {})

goal (1 subgoal):
 1. \<phi> 0 x = 1
[PROOF STEP]
have "x \<notin> V 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> V 1
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> A

goal (1 subgoal):
 1. x \<notin> V 1
[PROOF STEP]
by (auto simp: V_def)
[PROOF STATE]
proof (state)
this:
x \<notin> V 1

goal (1 subgoal):
 1. \<phi> 0 x = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> V 1
[PROOF STEP]
have "\<phi> (Suc 0) x = 0"
[PROOF STATE]
proof (prove)
using this:
x \<notin> V 1

goal (1 subgoal):
 1. \<phi> (Suc 0) x = 0
[PROOF STEP]
using \<phi>(5)[of 1] assms that
[PROOF STATE]
proof (prove)
using this:
x \<notin> V 1
1 \<in> {0, 1} \<Longrightarrow> csupport_on carrier (\<phi> 1) \<inter> carrier \<subseteq> V 1
closedin (top_of_set carrier) A
A \<subseteq> U
U \<subseteq> carrier
open U
x \<in> A

goal (1 subgoal):
 1. \<phi> (Suc 0) x = 0
[PROOF STEP]
by (auto simp: support_on_def csupport_on_def)
[PROOF STATE]
proof (state)
this:
\<phi> (Suc 0) x = 0

goal (1 subgoal):
 1. \<phi> 0 x = 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 = (\<Sum>i | i \<in> {0, 1} \<and> \<phi> i x \<noteq> 0. \<phi> i x)
{i \<in> {0, 1}. \<phi> i x \<noteq> 0} = (if \<phi> 0 x \<noteq> 0 then {0} else {}) \<union> (if \<phi> 1 x \<noteq> 0 then {1} else {})
\<phi> (Suc 0) x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 = (\<Sum>i | i \<in> {0, 1} \<and> \<phi> i x \<noteq> 0. \<phi> i x)
{i \<in> {0, 1}. \<phi> i x \<noteq> 0} = (if \<phi> 0 x \<noteq> 0 then {0} else {}) \<union> (if \<phi> 1 x \<noteq> 0 then {1} else {})
\<phi> (Suc 0) x = 0

goal (1 subgoal):
 1. \<phi> 0 x = 1
[PROOF STEP]
by (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
\<phi> 0 x = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x2 \<in> A \<Longrightarrow> \<phi> 0 ?x2 = 1

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>diff_fun k charts \<psi>; \<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<psi> x; \<And>x. x \<in> carrier \<Longrightarrow> \<psi> x \<le> 1; \<And>x. x \<in> A \<Longrightarrow> \<psi> x = 1; csupport_on carrier \<psi> \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
diff_fun k charts (\<phi> 0)
?x2 \<in> carrier \<Longrightarrow> 0 \<le> \<phi> 0 ?x2
?x2 \<in> carrier \<Longrightarrow> \<phi> 0 ?x2 \<le> 1
csupport_on carrier (\<phi> 0) \<inter> carrier \<subseteq> U
?x2 \<in> A \<Longrightarrow> \<phi> 0 ?x2 = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
diff_fun k charts (\<phi> 0)
?x2 \<in> carrier \<Longrightarrow> 0 \<le> \<phi> 0 ?x2
?x2 \<in> carrier \<Longrightarrow> \<phi> 0 ?x2 \<le> 1
csupport_on carrier (\<phi> 0) \<inter> carrier \<subseteq> U
?x2 \<in> A \<Longrightarrow> \<phi> 0 ?x2 = 1

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diff_fun_onE:
  assumes "diff_fun_on A f"
  obtains W f' where
    "A \<subseteq> W" "W \<subseteq> carrier" "open W" "diff_fun k (charts_submanifold W) f'"
    "\<And>x. x \<in> A \<Longrightarrow> f x = f' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>W f'. \<lbrakk>A \<subseteq> W; W \<subseteq> carrier; open W; diff_fun k (charts_submanifold W) f'; \<And>x. x \<in> A \<Longrightarrow> f x = f' x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
diff_fun_on A f

goal (1 subgoal):
 1. (\<And>W f'. \<lbrakk>A \<subseteq> W; W \<subseteq> carrier; open W; diff_fun k (charts_submanifold W) f'; \<And>x. x \<in> A \<Longrightarrow> f x = f' x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: diff_fun_on_def)


[STATEMENT]
lemma diff_fun_onI:
  assumes  "A \<subseteq> W" "W \<subseteq> carrier" "open W" "diff_fun k (charts_submanifold W) f'"
    "\<And>x. x \<in> A \<Longrightarrow> f x = f' x"
  shows "diff_fun_on A f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun_on A f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> W
W \<subseteq> carrier
open W
diff_fun k (charts_submanifold W) f'
?x3 \<in> A \<Longrightarrow> f ?x3 = f' ?x3

goal (1 subgoal):
 1. diff_fun_on A f
[PROOF STEP]
by (auto simp: diff_fun_on_def)


[STATEMENT]
lemma extension_lemmaE:
  fixes f::"'a \<Rightarrow> 'e::euclidean_space"
  assumes "closedin (top_of_set carrier) A"
  assumes "diff_fun_on A f" "A \<subseteq> U" "U \<subseteq> carrier" "open U"
  obtains f' where
    "diff_fun k charts f'"
    "\<And>x. x \<in> A \<Longrightarrow> f' x = f x"
    "csupport_on carrier f' \<inter> carrier \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from diff_fun_onE[OF assms(2)]
[PROOF STATE]
proof (chain)
picking this:
(\<And>W f'. \<lbrakk>A \<subseteq> W; W \<subseteq> carrier; open W; diff_fun k (charts_submanifold W) f'; \<And>x. x \<in> A \<Longrightarrow> f x = f' x\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain W' f' where W': "A \<subseteq> W'" "W' \<subseteq> carrier" "open W'" "diff_fun k (charts_submanifold W') f'"
    "(\<And>x. x \<in> A \<Longrightarrow> f x = f' x)"
[PROOF STATE]
proof (prove)
using this:
(\<And>W f'. \<lbrakk>A \<subseteq> W; W \<subseteq> carrier; open W; diff_fun k (charts_submanifold W) f'; \<And>x. x \<in> A \<Longrightarrow> f x = f' x\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>W' f'. \<lbrakk>A \<subseteq> W'; W' \<subseteq> carrier; open W'; diff_fun k (charts_submanifold W') f'; \<And>x. x \<in> A \<Longrightarrow> f x = f' x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A \<subseteq> W'
W' \<subseteq> carrier
open W'
diff_fun k (charts_submanifold W') f'
?x3 \<in> A \<Longrightarrow> f ?x3 = f' ?x3

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define W where "W = W' \<inter> U"
[PROOF STATE]
proof (state)
this:
W = W' \<inter> U

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret W': diff_fun k "charts_submanifold W'" f'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k (charts_submanifold W') f'
[PROOF STEP]
using W'
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> W'
W' \<subseteq> carrier
open W'
diff_fun k (charts_submanifold W') f'
?x3 \<in> A \<Longrightarrow> f ?x3 = f' ?x3

goal (1 subgoal):
 1. diff_fun k (charts_submanifold W') f'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have *: "open (W' \<inter> U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (W' \<inter> U)
[PROOF STEP]
using W' assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> W'
W' \<subseteq> carrier
open W'
diff_fun k (charts_submanifold W') f'
?x3 \<in> A \<Longrightarrow> f ?x3 = f' ?x3
closedin (top_of_set carrier) A
diff_fun_on A f
A \<subseteq> U
U \<subseteq> carrier
open U

goal (1 subgoal):
 1. open (W' \<inter> U)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
open (W' \<inter> U)

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with W'.diff_fun_submanifold[of W]
[PROOF STATE]
proof (chain)
picking this:
open W \<Longrightarrow> diff_fun k (W'.src.charts_submanifold W) f'
open (W' \<inter> U)
[PROOF STEP]
have "diff_fun k (W'.src.charts_submanifold (W' \<inter> U)) f'"
[PROOF STATE]
proof (prove)
using this:
open W \<Longrightarrow> diff_fun k (W'.src.charts_submanifold W) f'
open (W' \<inter> U)

goal (1 subgoal):
 1. diff_fun k (W'.src.charts_submanifold (W' \<inter> U)) f'
[PROOF STEP]
by (auto simp: W_def)
[PROOF STATE]
proof (state)
this:
diff_fun k (W'.src.charts_submanifold (W' \<inter> U)) f'

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
diff_fun k (W'.src.charts_submanifold (W' \<inter> U)) f'

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "W'.src.charts_submanifold (W' \<inter> U) = charts_submanifold (W' \<inter> U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W'.src.charts_submanifold (W' \<inter> U) = charts_submanifold (W' \<inter> U)
[PROOF STEP]
unfolding W'.src.charts_submanifold_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict_chart (W' \<inter> U) ` charts_submanifold W' = charts_submanifold (W' \<inter> U)
[PROOF STEP]
unfolding charts_submanifold_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict_chart (W' \<inter> U) ` restrict_chart W' ` charts = restrict_chart (W' \<inter> U) ` charts
[PROOF STEP]
using W' *
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> W'
W' \<subseteq> carrier
open W'
diff_fun k (charts_submanifold W') f'
?x3 \<in> A \<Longrightarrow> f ?x3 = f' ?x3
open (W' \<inter> U)

goal (1 subgoal):
 1. restrict_chart (W' \<inter> U) ` restrict_chart W' ` charts = restrict_chart (W' \<inter> U) ` charts
[PROOF STEP]
by (auto simp: image_image restrict_chart_restrict_chart ac_simps)
[PROOF STATE]
proof (state)
this:
W'.src.charts_submanifold (W' \<inter> U) = charts_submanifold (W' \<inter> U)

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
diff_fun k (charts_submanifold (W' \<inter> U)) f'
[PROOF STEP]
have "diff_fun k (charts_submanifold (W' \<inter> U)) f'"
[PROOF STATE]
proof (prove)
using this:
diff_fun k (charts_submanifold (W' \<inter> U)) f'

goal (1 subgoal):
 1. diff_fun k (charts_submanifold (W' \<inter> U)) f'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
diff_fun k (charts_submanifold (W' \<inter> U)) f'

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with W' assms
[PROOF STATE]
proof (chain)
picking this:
A \<subseteq> W'
W' \<subseteq> carrier
open W'
diff_fun k (charts_submanifold W') f'
?x3 \<in> A \<Longrightarrow> f ?x3 = f' ?x3
closedin (top_of_set carrier) A
diff_fun_on A f
A \<subseteq> U
U \<subseteq> carrier
open U
diff_fun k (charts_submanifold (W' \<inter> U)) f'
[PROOF STEP]
have W: "A \<subseteq> W" "W \<subseteq> carrier" "open W" "diff_fun k (charts_submanifold W) f'"
    "(\<And>x. x \<in> A \<Longrightarrow> f x = f' x)"
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> W'
W' \<subseteq> carrier
open W'
diff_fun k (charts_submanifold W') f'
?x3 \<in> A \<Longrightarrow> f ?x3 = f' ?x3
closedin (top_of_set carrier) A
diff_fun_on A f
A \<subseteq> U
U \<subseteq> carrier
open U
diff_fun k (charts_submanifold (W' \<inter> U)) f'

goal (1 subgoal):
 1. (A \<subseteq> W &&& W \<subseteq> carrier) &&& open W &&& diff_fun k (charts_submanifold W) f' &&& (\<And>x. x \<in> A \<Longrightarrow> f x = f' x)
[PROOF STEP]
by (auto simp: W_def)
[PROOF STATE]
proof (state)
this:
A \<subseteq> W
W \<subseteq> carrier
open W
diff_fun k (charts_submanifold W) f'
?x3 \<in> A \<Longrightarrow> f ?x3 = f' ?x3

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret submanifold _ _ W
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submanifold charts k W
[PROOF STEP]
by unfold_locales fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret W: diff_fun k "(charts_submanifold W)" f'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k (charts_submanifold W) f'
[PROOF STEP]
using W
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> W
W \<subseteq> carrier
open W
diff_fun k (charts_submanifold W) f'
?x3 \<in> A \<Longrightarrow> f ?x3 = f' ?x3

goal (1 subgoal):
 1. diff_fun k (charts_submanifold W) f'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have [simp]: "sub.carrier = W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub.carrier = W
[PROOF STEP]
using \<open>W \<subseteq> carrier\<close>
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> carrier

goal (1 subgoal):
 1. sub.carrier = W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sub.carrier = W

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "W \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W \<subseteq> U
[PROOF STEP]
by (auto simp: W_def)
[PROOF STATE]
proof (state)
this:
W \<subseteq> U

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from smooth_bump_functionE[OF assms(1) \<open>A \<subseteq> W\<close> \<open>W \<subseteq> carrier\<close> \<open>open W\<close>]
[PROOF STATE]
proof (chain)
picking this:
(\<And>\<psi>. \<lbrakk>diff_fun k charts \<psi>; \<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<psi> x; \<And>x. x \<in> carrier \<Longrightarrow> \<psi> x \<le> 1; \<And>x. x \<in> A \<Longrightarrow> \<psi> x = 1; csupport_on carrier \<psi> \<inter> carrier \<subseteq> W\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain \<phi>::"'a\<Rightarrow>real" where \<phi>: "diff_fun k charts \<phi>"
    "(\<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<phi> x)" "(\<And>x. x \<in> carrier \<Longrightarrow> \<phi> x \<le> 1)" "(\<And>x. x \<in> A \<Longrightarrow> \<phi> x = 1)"
    "csupport_on carrier \<phi> \<inter> carrier \<subseteq> W"
[PROOF STATE]
proof (prove)
using this:
(\<And>\<psi>. \<lbrakk>diff_fun k charts \<psi>; \<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<psi> x; \<And>x. x \<in> carrier \<Longrightarrow> \<psi> x \<le> 1; \<And>x. x \<in> A \<Longrightarrow> \<psi> x = 1; csupport_on carrier \<psi> \<inter> carrier \<subseteq> W\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>diff_fun k charts \<phi>; \<And>x. x \<in> carrier \<Longrightarrow> 0 \<le> \<phi> x; \<And>x. x \<in> carrier \<Longrightarrow> \<phi> x \<le> 1; \<And>x. x \<in> A \<Longrightarrow> \<phi> x = 1; csupport_on carrier \<phi> \<inter> carrier \<subseteq> W\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
diff_fun k charts \<phi>
?x3 \<in> carrier \<Longrightarrow> 0 \<le> \<phi> ?x3
?x3 \<in> carrier \<Longrightarrow> \<phi> ?x3 \<le> 1
?x3 \<in> A \<Longrightarrow> \<phi> ?x3 = 1
csupport_on carrier \<phi> \<inter> carrier \<subseteq> W

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret \<phi>: diff_fun k charts \<phi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k charts \<phi>
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define g where "g p = (if p \<in> W then \<phi> p *\<^sub>R f' p else 0)" for p
[PROOF STATE]
proof (state)
this:
g ?p = (if ?p \<in> W then \<phi> ?p *\<^sub>R f' ?p else (0::'e))

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thm sub.diff_fun_scaleR
[PROOF STATE]
proof (state)
this:
g ?p = (if ?p \<in> W then \<phi> ?p *\<^sub>R f' ?p else (0::'e))

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "diff_fun k charts g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k charts g
[PROOF STEP]
proof (rule manifold_eucl.diff_open_Un, unfold diff_fun_def[symmetric])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. diff_fun k (charts_submanifold ?U) g
 2. diff_fun k (charts_submanifold ?V) g
 3. open ?U
 4. open ?V
 5. carrier \<subseteq> ?U \<union> ?V
[PROOF STEP]
have "diff_fun k (charts_submanifold W) (\<lambda>p. \<phi> p *\<^sub>R f' p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k (charts_submanifold W) (\<lambda>p. \<phi> p *\<^sub>R f' p)
[PROOF STEP]
by (auto intro!: sub.diff_fun_scaleR \<phi>.diff_fun_submanifold W)
[PROOF STATE]
proof (state)
this:
diff_fun k (charts_submanifold W) (\<lambda>p. \<phi> p *\<^sub>R f' p)

goal (5 subgoals):
 1. diff_fun k (charts_submanifold ?U) g
 2. diff_fun k (charts_submanifold ?V) g
 3. open ?U
 4. open ?V
 5. carrier \<subseteq> ?U \<union> ?V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
diff_fun k (charts_submanifold W) (\<lambda>p. \<phi> p *\<^sub>R f' p)
[PROOF STEP]
show "diff_fun k (charts_submanifold W) g"
[PROOF STATE]
proof (prove)
using this:
diff_fun k (charts_submanifold W) (\<lambda>p. \<phi> p *\<^sub>R f' p)

goal (1 subgoal):
 1. diff_fun k (charts_submanifold W) g
[PROOF STEP]
by (rule diff_fun.diff_fun_cong) (auto simp: g_def)
[PROOF STATE]
proof (state)
this:
diff_fun k (charts_submanifold W) g

goal (4 subgoals):
 1. diff_fun k (charts_submanifold ?V) g
 2. open W
 3. open ?V
 4. carrier \<subseteq> W \<union> ?V
[PROOF STEP]
interpret C: submanifold _ _ "carrier - csupport_on carrier \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submanifold charts k (carrier - csupport_on carrier \<phi>)
[PROOF STEP]
by unfold_locales auto
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. diff_fun k (charts_submanifold ?V) g
 2. open W
 3. open ?V
 4. carrier \<subseteq> W \<union> ?V
[PROOF STEP]
have sub_carrier[simp]: "C.sub.carrier = carrier - csupport_on carrier \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.sub.carrier = carrier - csupport_on carrier \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C.sub.carrier = carrier - csupport_on carrier \<phi>

goal (4 subgoals):
 1. diff_fun k (charts_submanifold ?V) g
 2. open W
 3. open ?V
 4. carrier \<subseteq> W \<union> ?V
[PROOF STEP]
have "diff_fun k (charts_submanifold (carrier - csupport_on carrier \<phi>)) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k (charts_submanifold (carrier - csupport_on carrier \<phi>)) 0
[PROOF STEP]
by (rule C.sub.diff_fun_zero)
[PROOF STATE]
proof (state)
this:
diff_fun k (charts_submanifold (carrier - csupport_on carrier \<phi>)) 0

goal (4 subgoals):
 1. diff_fun k (charts_submanifold ?V) g
 2. open W
 3. open ?V
 4. carrier \<subseteq> W \<union> ?V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
diff_fun k (charts_submanifold (carrier - csupport_on carrier \<phi>)) 0
[PROOF STEP]
show "diff_fun k (charts_submanifold (carrier - csupport_on carrier \<phi>)) g"
[PROOF STATE]
proof (prove)
using this:
diff_fun k (charts_submanifold (carrier - csupport_on carrier \<phi>)) 0

goal (1 subgoal):
 1. diff_fun k (charts_submanifold (carrier - csupport_on carrier \<phi>)) g
[PROOF STEP]
by (rule diff_fun.diff_fun_cong) (auto simp: g_def not_in_csupportD)
[PROOF STATE]
proof (state)
this:
diff_fun k (charts_submanifold (carrier - csupport_on carrier \<phi>)) g

goal (3 subgoals):
 1. open W
 2. open (carrier - csupport_on carrier \<phi>)
 3. carrier \<subseteq> W \<union> (carrier - csupport_on carrier \<phi>)
[PROOF STEP]
show "open W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open W
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
open W

goal (2 subgoals):
 1. open (carrier - csupport_on carrier \<phi>)
 2. carrier \<subseteq> W \<union> (carrier - csupport_on carrier \<phi>)
[PROOF STEP]
show "open (carrier - csupport_on carrier \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (carrier - csupport_on carrier \<phi>)
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
open (carrier - csupport_on carrier \<phi>)

goal (1 subgoal):
 1. carrier \<subseteq> W \<union> (carrier - csupport_on carrier \<phi>)
[PROOF STEP]
show "carrier \<subseteq> W \<union> (carrier - csupport_on carrier \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. carrier \<subseteq> W \<union> (carrier - csupport_on carrier \<phi>)
[PROOF STEP]
using \<phi>
[PROOF STATE]
proof (prove)
using this:
diff_fun k charts \<phi>
?x3 \<in> carrier \<Longrightarrow> 0 \<le> \<phi> ?x3
?x3 \<in> carrier \<Longrightarrow> \<phi> ?x3 \<le> 1
?x3 \<in> A \<Longrightarrow> \<phi> ?x3 = 1
csupport_on carrier \<phi> \<inter> carrier \<subseteq> W

goal (1 subgoal):
 1. carrier \<subseteq> W \<union> (carrier - csupport_on carrier \<phi>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
carrier \<subseteq> W \<union> (carrier - csupport_on carrier \<phi>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
diff_fun k charts g

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
diff_fun k charts g

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<And>x. x \<in> A \<Longrightarrow> g x = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> g x = f x
[PROOF STEP]
using \<open>A \<subseteq> W\<close>
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> W

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> g x = f x
[PROOF STEP]
by (auto simp: g_def \<phi> W')
[PROOF STATE]
proof (state)
this:
?x3 \<in> A \<Longrightarrow> g ?x3 = f ?x3

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x3 \<in> A \<Longrightarrow> g ?x3 = f ?x3

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "csupport_on carrier g \<inter> carrier  \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. csupport_on carrier g \<inter> carrier \<subseteq> U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. csupport_on carrier g \<inter> carrier \<subseteq> U
[PROOF STEP]
have "csupport_on carrier g \<subseteq> csupport_on carrier \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. csupport_on carrier g \<subseteq> csupport_on carrier \<phi>
[PROOF STEP]
by (rule csupport_on_mono) (auto simp: g_def[abs_def] split: if_splits)
[PROOF STATE]
proof (state)
this:
csupport_on carrier g \<subseteq> csupport_on carrier \<phi>

goal (1 subgoal):
 1. csupport_on carrier g \<inter> carrier \<subseteq> U
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
csupport_on carrier g \<subseteq> csupport_on carrier \<phi>

goal (1 subgoal):
 1. csupport_on carrier g \<inter> carrier \<subseteq> U
[PROOF STEP]
have "\<dots>  \<inter> carrier \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. csupport_on carrier \<phi> \<inter> carrier \<subseteq> U
[PROOF STEP]
using \<phi>(5) \<open>W \<subseteq> U\<close> \<open>W \<subseteq> carrier\<close> \<open>U \<subseteq> carrier\<close>
[PROOF STATE]
proof (prove)
using this:
csupport_on carrier \<phi> \<inter> carrier \<subseteq> W
W \<subseteq> U
W \<subseteq> carrier
U \<subseteq> carrier

goal (1 subgoal):
 1. csupport_on carrier \<phi> \<inter> carrier \<subseteq> U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
csupport_on carrier \<phi> \<inter> carrier \<subseteq> U

goal (1 subgoal):
 1. csupport_on carrier g \<inter> carrier \<subseteq> U
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<subseteq> y \<Longrightarrow> x \<inter> carrier \<subseteq> y \<inter> carrier) \<Longrightarrow> csupport_on carrier g \<inter> carrier \<subseteq> U
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<subseteq> y \<Longrightarrow> x \<inter> carrier \<subseteq> y \<inter> carrier) \<Longrightarrow> csupport_on carrier g \<inter> carrier \<subseteq> U

goal (1 subgoal):
 1. csupport_on carrier g \<inter> carrier \<subseteq> U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
csupport_on carrier g \<inter> carrier \<subseteq> U

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
csupport_on carrier g \<inter> carrier \<subseteq> U

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>diff_fun k charts f'; \<And>x. x \<in> A \<Longrightarrow> f' x = f x; csupport_on carrier f' \<inter> carrier \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
diff_fun k charts g
?x3 \<in> A \<Longrightarrow> g ?x3 = f ?x3
csupport_on carrier g \<inter> carrier \<subseteq> U
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
diff_fun k charts g
?x3 \<in> A \<Longrightarrow> g ?x3 = f ?x3
csupport_on carrier g \<inter> carrier \<subseteq> U

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma HNextPart_Inv1: "\<lbrakk> HInv1 s; HNextPart s s'; Inv1 s' \<rbrakk> \<Longrightarrow> HInv1 s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>HInv1 s; HNextPart s s'; Inv1 s'\<rbrakk> \<Longrightarrow> HInv1 s'
[PROOF STEP]
by(auto simp add: HNextPart_def Inv1_def)


[STATEMENT]
theorem HInit_HInv1: "HInit s \<longrightarrow> HInv1 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInit s \<longrightarrow> HInv1 s
[PROOF STEP]
by(auto simp add: HInit_def Inv1_def Init_def allRdBlks_def)


[STATEMENT]
lemma allRdBlks_finite:
  assumes inv: "HInv1 s"
  and     asm: "\<forall>p. allRdBlks s' p \<subseteq> insert bk (allRdBlks s p)"
  shows   "\<forall>p. finite (allRdBlks s' p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. finite (allRdBlks s' p)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. finite (allRdBlks s' p)
[PROOF STEP]
fix pp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. finite (allRdBlks s' p)
[PROOF STEP]
from inv
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
[PROOF STEP]
have "\<forall>p. finite (allRdBlks s p)"
[PROOF STATE]
proof (prove)
using this:
HInv1 s

goal (1 subgoal):
 1. \<forall>p. finite (allRdBlks s p)
[PROOF STEP]
by(simp add: Inv1_def)
[PROOF STATE]
proof (state)
this:
\<forall>p. finite (allRdBlks s p)

goal (1 subgoal):
 1. \<And>p. finite (allRdBlks s' p)
[PROOF STEP]
hence "finite (allRdBlks s pp)"
[PROOF STATE]
proof (prove)
using this:
\<forall>p. finite (allRdBlks s p)

goal (1 subgoal):
 1. finite (allRdBlks s pp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (allRdBlks s pp)

goal (1 subgoal):
 1. \<And>p. finite (allRdBlks s' p)
[PROOF STEP]
with asm
[PROOF STATE]
proof (chain)
picking this:
\<forall>p. allRdBlks s' p \<subseteq> insert bk (allRdBlks s p)
finite (allRdBlks s pp)
[PROOF STEP]
show "finite (allRdBlks s' pp)"
[PROOF STATE]
proof (prove)
using this:
\<forall>p. allRdBlks s' p \<subseteq> insert bk (allRdBlks s p)
finite (allRdBlks s pp)

goal (1 subgoal):
 1. finite (allRdBlks s' pp)
[PROOF STEP]
by (auto intro: finite_subset)
[PROOF STATE]
proof (state)
this:
finite (allRdBlks s' pp)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem HPhase1or2ReadThen_HInv1:
  assumes inv1: "HInv1 s"
  and act: "HPhase1or2ReadThen s s' p d q"
  shows "HInv1 s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
proof -
  \<comment> \<open>we focus on the last conjunct of Inv1\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
from act
[PROOF STATE]
proof (chain)
picking this:
HPhase1or2ReadThen s s' p d q
[PROOF STEP]
have "\<forall>p. allRdBlks s' p \<subseteq> allRdBlks s p \<union> {\<lparr>block = disk s d q, proc = q\<rparr>}"
[PROOF STATE]
proof (prove)
using this:
HPhase1or2ReadThen s s' p d q

goal (1 subgoal):
 1. \<forall>p. allRdBlks s' p \<subseteq> allRdBlks s p \<union> {\<lparr>block = disk s d q, proc = q\<rparr>}
[PROOF STEP]
by(auto simp add: Phase1or2ReadThen_def allRdBlks_def
               split: if_split_asm)
[PROOF STATE]
proof (state)
this:
\<forall>p. allRdBlks s' p \<subseteq> allRdBlks s p \<union> {\<lparr>block = disk s d q, proc = q\<rparr>}

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
with inv1
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
\<forall>p. allRdBlks s' p \<subseteq> allRdBlks s p \<union> {\<lparr>block = disk s d q, proc = q\<rparr>}
[PROOF STEP]
have "\<forall>p. finite (allRdBlks s' p)"
[PROOF STATE]
proof (prove)
using this:
HInv1 s
\<forall>p. allRdBlks s' p \<subseteq> allRdBlks s p \<union> {\<lparr>block = disk s d q, proc = q\<rparr>}

goal (1 subgoal):
 1. \<forall>p. finite (allRdBlks s' p)
[PROOF STEP]
by(blast dest: allRdBlks_finite)
  \<comment> \<open>the others conjuncts are trivial\<close>
[PROOF STATE]
proof (state)
this:
\<forall>p. finite (allRdBlks s' p)

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
with inv1 act
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
HPhase1or2ReadThen s s' p d q
\<forall>p. finite (allRdBlks s' p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
HInv1 s
HPhase1or2ReadThen s s' p d q
\<forall>p. finite (allRdBlks s' p)

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
by(auto simp add: Inv1_def Phase1or2ReadThen_def HNextPart_def)
[PROOF STATE]
proof (state)
this:
HInv1 s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem HEndPhase1_HInv1:
  assumes inv1: "HInv1 s"
  and act: "HEndPhase1 s s' p"
  shows "HInv1 s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
from inv1 act
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
HEndPhase1 s s' p
[PROOF STEP]
have "Inv1 s'"
[PROOF STATE]
proof (prove)
using this:
HInv1 s
HEndPhase1 s s' p

goal (1 subgoal):
 1. Inv1 s'
[PROOF STEP]
by(auto simp add:  Inv1_def EndPhase1_def InitializePhase_def allRdBlks_def)
[PROOF STATE]
proof (state)
this:
Inv1 s'

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
with inv1 act
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
HEndPhase1 s s' p
Inv1 s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
HInv1 s
HEndPhase1 s s' p
Inv1 s'

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
by(auto simp del: HInv1_def dest: HNextPart_Inv1)
[PROOF STATE]
proof (state)
this:
HInv1 s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem HStartBallot_HInv1:
  assumes inv1: "HInv1 s"
  and act: "HStartBallot s s' p"
  shows "HInv1 s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
from inv1 act
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
HStartBallot s s' p
[PROOF STEP]
have "Inv1 s'"
[PROOF STATE]
proof (prove)
using this:
HInv1 s
HStartBallot s s' p

goal (1 subgoal):
 1. Inv1 s'
[PROOF STEP]
by(auto simp add: Inv1_def StartBallot_def InitializePhase_def allRdBlks_def)
[PROOF STATE]
proof (state)
this:
Inv1 s'

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
with inv1 act
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
HStartBallot s s' p
Inv1 s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
HInv1 s
HStartBallot s s' p
Inv1 s'

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
by(auto simp del: HInv1_def elim: HNextPart_Inv1)
[PROOF STATE]
proof (state)
this:
HInv1 s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem HPhase1or2Write_HInv1:
  assumes inv1: "HInv1 s"
  and act: "HPhase1or2Write s s' p d"
  shows "HInv1 s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
from inv1 act
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
HPhase1or2Write s s' p d
[PROOF STEP]
have "Inv1 s'"
[PROOF STATE]
proof (prove)
using this:
HInv1 s
HPhase1or2Write s s' p d

goal (1 subgoal):
 1. Inv1 s'
[PROOF STEP]
by(auto simp add: Inv1_def Phase1or2Write_def allRdBlks_def)
[PROOF STATE]
proof (state)
this:
Inv1 s'

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
with inv1 act
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
HPhase1or2Write s s' p d
Inv1 s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
HInv1 s
HPhase1or2Write s s' p d
Inv1 s'

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
by(auto simp del: HInv1_def elim: HNextPart_Inv1)
[PROOF STATE]
proof (state)
this:
HInv1 s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem HPhase1or2ReadElse_HInv1:
  assumes act: "HPhase1or2ReadElse s s' p d q"
  and inv1: "HInv1 s"
  shows "HInv1 s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
using HStartBallot_HInv1[OF inv1] act
[PROOF STATE]
proof (prove)
using this:
HStartBallot s ?s' ?p \<Longrightarrow> HInv1 ?s'
HPhase1or2ReadElse s s' p d q

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
by(auto simp add: Phase1or2ReadElse_def)


[STATEMENT]
theorem HEndPhase2_HInv1:
  assumes inv1: "HInv1 s"
  and  act: "HEndPhase2 s s' p"
  shows "HInv1 s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
from inv1 act
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
HEndPhase2 s s' p
[PROOF STEP]
have "Inv1 s'"
[PROOF STATE]
proof (prove)
using this:
HInv1 s
HEndPhase2 s s' p

goal (1 subgoal):
 1. Inv1 s'
[PROOF STEP]
by(auto simp add: Inv1_def EndPhase2_def InitializePhase_def allRdBlks_def)
[PROOF STATE]
proof (state)
this:
Inv1 s'

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
with inv1 act
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
HEndPhase2 s s' p
Inv1 s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
HInv1 s
HEndPhase2 s s' p
Inv1 s'

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
by(auto simp del: HInv1_def elim: HNextPart_Inv1)
[PROOF STATE]
proof (state)
this:
HInv1 s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem HFail_HInv1:
  assumes inv1: "HInv1 s"
  and     act: "HFail s s' p"
  shows "HInv1 s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
from inv1 act
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
HFail s s' p
[PROOF STEP]
have "Inv1 s'"
[PROOF STATE]
proof (prove)
using this:
HInv1 s
HFail s s' p

goal (1 subgoal):
 1. Inv1 s'
[PROOF STEP]
by(auto simp add: Inv1_def Fail_def InitializePhase_def allRdBlks_def)
[PROOF STATE]
proof (state)
this:
Inv1 s'

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
with inv1 act
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
HFail s s' p
Inv1 s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
HInv1 s
HFail s s' p
Inv1 s'

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
by(auto simp del: HInv1_def elim: HNextPart_Inv1)
[PROOF STATE]
proof (state)
this:
HInv1 s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem HPhase0Read_HInv1:
  assumes inv1: "HInv1 s"
  and     act: "HPhase0Read s s' p d"
  shows "HInv1 s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
proof -
 \<comment> \<open>we focus on the last conjunct of Inv1\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
from act
[PROOF STATE]
proof (chain)
picking this:
HPhase0Read s s' p d
[PROOF STEP]
have "\<forall>pp. allRdBlks s' pp \<subseteq> allRdBlks s pp \<union> {\<lparr>block = disk s d p, proc = p\<rparr>}"
[PROOF STATE]
proof (prove)
using this:
HPhase0Read s s' p d

goal (1 subgoal):
 1. \<forall>pp. allRdBlks s' pp \<subseteq> allRdBlks s pp \<union> {\<lparr>block = disk s d p, proc = p\<rparr>}
[PROOF STEP]
by(auto simp add: Phase0Read_def allRdBlks_def
               split: if_split_asm)
[PROOF STATE]
proof (state)
this:
\<forall>pp. allRdBlks s' pp \<subseteq> allRdBlks s pp \<union> {\<lparr>block = disk s d p, proc = p\<rparr>}

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
with inv1
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
\<forall>pp. allRdBlks s' pp \<subseteq> allRdBlks s pp \<union> {\<lparr>block = disk s d p, proc = p\<rparr>}
[PROOF STEP]
have "\<forall>p. finite (allRdBlks s' p)"
[PROOF STATE]
proof (prove)
using this:
HInv1 s
\<forall>pp. allRdBlks s' pp \<subseteq> allRdBlks s pp \<union> {\<lparr>block = disk s d p, proc = p\<rparr>}

goal (1 subgoal):
 1. \<forall>p. finite (allRdBlks s' p)
[PROOF STEP]
by(blast dest: allRdBlks_finite)
  \<comment> \<open>the others conjuncts are trivial\<close>
[PROOF STATE]
proof (state)
this:
\<forall>p. finite (allRdBlks s' p)

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
with inv1 act
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
HPhase0Read s s' p d
\<forall>p. finite (allRdBlks s' p)
[PROOF STEP]
have "Inv1 s'"
[PROOF STATE]
proof (prove)
using this:
HInv1 s
HPhase0Read s s' p d
\<forall>p. finite (allRdBlks s' p)

goal (1 subgoal):
 1. Inv1 s'
[PROOF STEP]
by(auto simp add: Inv1_def Phase0Read_def)
[PROOF STATE]
proof (state)
this:
Inv1 s'

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
with inv1 act
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
HPhase0Read s s' p d
Inv1 s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
HInv1 s
HPhase0Read s s' p d
Inv1 s'

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
by(auto simp del: HInv1_def elim: HNextPart_Inv1)
[PROOF STATE]
proof (state)
this:
HInv1 s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem HEndPhase0_HInv1:
  assumes inv1: "HInv1 s"
  and act: "HEndPhase0 s s' p"
  shows "HInv1 s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
from inv1 act
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
HEndPhase0 s s' p
[PROOF STEP]
have "Inv1 s'"
[PROOF STATE]
proof (prove)
using this:
HInv1 s
HEndPhase0 s s' p

goal (1 subgoal):
 1. Inv1 s'
[PROOF STEP]
by(auto simp add: Inv1_def EndPhase0_def allRdBlks_def InitializePhase_def)
[PROOF STATE]
proof (state)
this:
Inv1 s'

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
with inv1 act
[PROOF STATE]
proof (chain)
picking this:
HInv1 s
HEndPhase0 s s' p
Inv1 s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
HInv1 s
HEndPhase0 s s' p
Inv1 s'

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
by(auto simp del: HInv1_def elim: HNextPart_Inv1)
[PROOF STATE]
proof (state)
this:
HInv1 s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma I2a:
  assumes nxt: "HNext s s'"
  and inv: "HInv1 s"
  shows "HInv1 s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
HNext s s'
HInv1 s

goal (1 subgoal):
 1. HInv1 s'
[PROOF STEP]
by(auto
    simp add: HNext_def Next_def,
    auto intro: HStartBallot_HInv1,
    auto intro: HPhase0Read_HInv1,
    auto intro: HPhase1or2Write_HInv1,
    auto simp add: Phase1or2Read_def
         intro: HPhase1or2ReadThen_HInv1
                HPhase1or2ReadElse_HInv1,
    auto simp add: EndPhase1or2_def
         intro: HEndPhase1_HInv1
                HEndPhase2_HInv1,
    auto intro: HFail_HInv1,
    auto intro: HEndPhase0_HInv1)


[STATEMENT]
lemma expr'_rel_eq: "expr'_rel (=) e\<^sub>1 e\<^sub>2 \<longleftrightarrow> e\<^sub>1 = e\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expr'_rel (=) e\<^sub>1 e\<^sub>2 = (e\<^sub>1 = e\<^sub>2)
[PROOF STEP]
by(induct e\<^sub>1 e\<^sub>2 rule: expr'_rel.induct) simp_all


[STATEMENT]
lemma inj_expr [simp]: "inj Lit" "inj Var" "inj Add" "inj (Add e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inj Lit &&& inj Var) &&& inj Add &&& inj (Add e)
[PROOF STEP]
by(simp_all add: fun_eq_iff inj_on_def)


[STATEMENT]
lemma infinite_UNIV_expr: "\<not> finite (UNIV :: expr set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite UNIV
[PROOF STEP]
including card_datatype
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite UNIV
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite UNIV
[PROOF STEP]
have "rangeIt (Lit 0) (Add (Lit 0)) \<subseteq> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rangeIt (Lit 0) (Add (Lit 0)) \<subseteq> UNIV
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rangeIt (Lit 0) (Add (Lit 0)) \<subseteq> UNIV

goal (1 subgoal):
 1. infinite UNIV
[PROOF STEP]
from finite_subset[OF this]
[PROOF STATE]
proof (chain)
picking this:
finite UNIV \<Longrightarrow> finite (rangeIt (Lit 0) (Add (Lit 0)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite UNIV \<Longrightarrow> finite (rangeIt (Lit 0) (Add (Lit 0)))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_expr' [simp]: "inj Lit'" "inj Var'" "inj Add'" "inj (Add' e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inj Lit' &&& inj Var') &&& inj Add' &&& inj (Add' e)
[PROOF STEP]
by(simp_all add: fun_eq_iff inj_on_def)


[STATEMENT]
lemma infinite_UNIV_expr': "\<not> finite (UNIV :: 'a expr' set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite UNIV
[PROOF STEP]
including card_datatype
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite UNIV
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite UNIV
[PROOF STEP]
have "rangeIt (Lit' 0) (Add' (Lit' 0)) \<subseteq> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rangeIt (Lit' 0) (Add' (Lit' 0)) \<subseteq> UNIV
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rangeIt (Lit' 0) (Add' (Lit' 0)) \<subseteq> UNIV

goal (1 subgoal):
 1. infinite UNIV
[PROOF STEP]
from finite_subset[OF this]
[PROOF STATE]
proof (chain)
picking this:
finite UNIV \<Longrightarrow> finite (rangeIt (Lit' 0) (Add' (Lit' 0)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite UNIV \<Longrightarrow> finite (rangeIt (Lit' 0) (Add' (Lit' 0)))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trie_keys_empty [code]: "trie_keys trie_empty = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trie_keys trie_empty = {}
[PROOF STEP]
by(simp add: trie_keys_dom_lookup trie_lookup_empty)


[STATEMENT]
lemma trie_keys_update [code]:
  "trie_keys (trie_update k v t) = insert k (trie_keys t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trie_keys (trie_update k v t) = insert k (trie_keys t)
[PROOF STEP]
by(simp add: trie_keys_dom_lookup trie_lookup_update)


[STATEMENT]
lemma lookup_empty: "lookup empty = Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup Containers_Userguide.empty = Map.empty
[PROOF STEP]
by transfer(simp add: trie_lookup_empty fun_eq_iff)


[STATEMENT]
lemma lookup_update: "lookup (update k v t) = (lookup t)(k \<mapsto> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (update k v t) = lookup t(k \<mapsto> v)
[PROOF STEP]
using ID_cbl
[PROOF STATE]
proof (prove)
using this:
ID cbl \<noteq> None

goal (1 subgoal):
 1. lookup (update k v t) = lookup t(k \<mapsto> v)
[PROOF STEP]
by transfer(auto simp add: trie_lookup_update fun_eq_iff dest: inj_to_bl[THEN injD])


[STATEMENT]
lemma keys_conv_dom_lookup: "keys t = dom (lookup t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys t = dom (lookup t)
[PROOF STEP]
using ID_cbl
[PROOF STATE]
proof (prove)
using this:
ID cbl \<noteq> None

goal (1 subgoal):
 1. keys t = dom (lookup t)
[PROOF STEP]
by transfer(force simp add: trie_keys_dom_lookup to_bl_inverse intro: rev_image_eqI)


[STATEMENT]
lemma lookup_Trie_Mapping [code]:
  "Mapping.lookup (Trie_Mapping t) = lookup t"
  \<comment> \<open>Lookup does not need the check on @{term cbl},
        because we have defined the pseudo-constructor @{term Trie_Mapping} in terms of @{term "lookup"}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup (Trie_Mapping t) = lookup t
[PROOF STEP]
by simp(transfer, simp)


[STATEMENT]
lemma update_Trie_Mapping [code]:
  "Mapping.update k v (Trie_Mapping t) =
  (case ID cbl :: 'k cbl of
     None \<Rightarrow> Code.abort (STR ''update Trie_Mapping: cbl = None'') (\<lambda>_. Mapping.update k v (Trie_Mapping t))
   | Some _ \<Rightarrow> Trie_Mapping (update k v t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.update k v (Trie_Mapping t) = (case ID cbl of None \<Rightarrow> Code.abort STR ''update Trie_Mapping: cbl = None'' (\<lambda>_. Mapping.update k v (Trie_Mapping t)) | Some x \<Rightarrow> Trie_Mapping (update k v t))
[PROOF STEP]
by(simp split: option.split add: lookup_update Mapping.update.abs_eq)


[STATEMENT]
lemma keys_Trie_Mapping [code]:
  "Mapping.keys (Trie_Mapping t) =
  (case ID cbl :: 'k cbl of
     None \<Rightarrow> Code.abort (STR ''keys Trie_Mapping: cbl = None'') (\<lambda>_. Mapping.keys (Trie_Mapping t))
   | Some _ \<Rightarrow> keys t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.keys (Trie_Mapping t) = (case ID cbl of None \<Rightarrow> Code.abort STR ''keys Trie_Mapping: cbl = None'' (\<lambda>_. Mapping.keys (Trie_Mapping t)) | Some x \<Rightarrow> keys t)
[PROOF STEP]
by(simp add: Mapping.keys.abs_eq keys_conv_dom_lookup split: option.split)


[STATEMENT]
lemma mapping_empty_choose_code [code]:
  "(mapping_empty_choose :: ('a :: {ccompare, cbl}, 'b) mapping) =
   (case ID CCOMPARE('a) of Some _  \<Rightarrow> RBT_Mapping RBT_Mapping2.empty
    | None \<Rightarrow>
      case ID (cbl :: 'a cbl) of Some _ \<Rightarrow> Trie_Mapping empty
      | None \<Rightarrow> Assoc_List_Mapping DAList.empty)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mapping_empty_choose = (case ID ccompare of None \<Rightarrow> case ID cbl of None \<Rightarrow> Assoc_List_Mapping DAList.empty | Some x \<Rightarrow> Trie_Mapping Containers_Userguide.empty | Some x \<Rightarrow> RBT_Mapping RBT_Mapping2.empty)
[PROOF STEP]
by(auto split: option.split simp add: DAList.lookup_empty[abs_def] Mapping.empty_def lookup_empty)


[STATEMENT]
lemma mapping_empty_code [code]:
  "mapping_empty mapping_Trie = Trie_Mapping empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mapping_empty mapping_Trie = Trie_Mapping Containers_Userguide.empty
[PROOF STEP]
by(simp add: lookup_empty Mapping.empty_def)


[STATEMENT]
lemma mapping_impl_choose2_Trie [code]:
  "mapping_impl_choose2 mapping_Trie mapping_Trie = mapping_Trie"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mapping_impl_choose2 mapping_Trie mapping_Trie = mapping_Trie
[PROOF STEP]
by(simp add: mapping_Trie_def)


[STATEMENT]
lemma mapping_impl_unit_Trie [code]:
  "MAPPING_IMPL(unit) = Phantom(unit) mapping_Trie"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mapping_impl = Phantom(unit) mapping_Trie
[PROOF STEP]
by(simp add: mapping_impl_unit_def)


[STATEMENT]
lemma empty_Set_Monad: "{} = Set_Monad []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} = Set_Monad []
[PROOF STEP]
by simp


[STATEMENT]
lemma ICdual:  "\<I> \<^bold>\<equiv> \<C>\<^sup>d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<^bold>\<equiv> \<C>\<^sup>d
[PROOF STEP]
using dual_symm equal_op_def
[PROOF STATE]
proof (prove)
using this:
?\<phi> \<equiv> ?\<psi>\<^sup>d \<Longrightarrow> ?\<psi> \<equiv> ?\<phi>\<^sup>d
?\<phi> \<^bold>\<equiv> ?\<psi> \<equiv> \<forall>X w. ?\<phi> X w = ?\<psi> X w

goal (1 subgoal):
 1. \<I> \<^bold>\<equiv> \<C>\<^sup>d
[PROOF STEP]
by auto


[STATEMENT]
lemma IB_rel: "Int_2 \<I> \<Longrightarrow> \<I> \<^bold>\<equiv> \<I>\<^sub>B \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<I> \<^bold>\<equiv> \<I>\<^sub>B \<B>
[PROOF STEP]
by (smt Br_int_def Int_br_def dEXP_def diff_def equal_op_def)


[STATEMENT]
lemma IF_rel: "Int_2 \<I> \<Longrightarrow> \<I> \<^bold>\<equiv> \<I>\<^sub>F \<F>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<I> \<^bold>\<equiv> \<I>\<^sub>F \<F>
[PROOF STEP]
using EXP_def EXP_dual2 Fr_int_def IB_rel Int_br_def Int_fr_def compl_def diff_def equal_op_def meet_def
[PROOF STATE]
proof (prove)
using this:
Cl_2 ?\<phi> \<equiv> \<forall>A. contains (?\<phi> A) A
Int_2 ?\<phi> \<Longrightarrow> Cl_2 ?\<phi>\<^sup>d
\<F>\<^sub>I ?\<I> \<equiv> ?\<I>\<^sup>c \<^bold>\<sqinter> ?\<I>\<^sup>d
Int_2 \<I> \<Longrightarrow> \<I> \<^bold>\<equiv> \<I>\<^sub>B \<B>
\<I>\<^sub>B ?\<B> \<equiv> \<lambda>A. A \<^bold>\<leftharpoonup> ?\<B> A
\<I>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<leftharpoonup> ?\<F> A
\<^bold>\<midarrow>?A \<equiv> \<lambda>w. \<not> ?A w
?A \<^bold>\<leftharpoonup> ?B \<equiv> \<lambda>w. ?A w \<and> \<not> ?B w
?\<phi> \<^bold>\<equiv> ?\<psi> \<equiv> \<forall>X w. ?\<phi> X w = ?\<psi> X w
?A \<^bold>\<and> ?B \<equiv> \<lambda>w. ?A w \<and> ?B w

goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<I> \<^bold>\<equiv> \<I>\<^sub>F \<F>
[PROOF STEP]
by fastforce


[STATEMENT]
lemma CB_rel: "Int_2 \<I> \<Longrightarrow> \<C> \<^bold>\<equiv> \<C>\<^sub>B \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<C> \<^bold>\<equiv> \<C>\<^sub>B \<B>
[PROOF STEP]
using Br_int_def Cl_br_def EXP_def EXP_dual2 compl_def diff_def dual_def equal_op_def join_def
[PROOF STATE]
proof (prove)
using this:
\<B>\<^sub>I ?\<I> \<equiv> \<lambda>A. A \<^bold>\<leftharpoonup> ?\<I> A
\<C>\<^sub>B ?\<B> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<B> (\<^bold>\<midarrow>A)
Cl_2 ?\<phi> \<equiv> \<forall>A. contains (?\<phi> A) A
Int_2 ?\<phi> \<Longrightarrow> Cl_2 ?\<phi>\<^sup>d
\<^bold>\<midarrow>?A \<equiv> \<lambda>w. \<not> ?A w
?A \<^bold>\<leftharpoonup> ?B \<equiv> \<lambda>w. ?A w \<and> \<not> ?B w
?\<phi>\<^sup>d \<equiv> \<lambda>X. ?\<phi>\<^sup>c (\<^bold>\<midarrow>X)
?\<phi> \<^bold>\<equiv> ?\<psi> \<equiv> \<forall>X w. ?\<phi> X w = ?\<psi> X w
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w

goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<C> \<^bold>\<equiv> \<C>\<^sub>B \<B>
[PROOF STEP]
by fastforce


[STATEMENT]
lemma CF_rel: "Int_2 \<I> \<Longrightarrow> \<C> \<^bold>\<equiv> \<C>\<^sub>F \<F>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<C> \<^bold>\<equiv> \<C>\<^sub>F \<F>
[PROOF STEP]
by (smt Cl_fr_def EXP_def EXP_dual2 Fr_int_def compl_def dEXP_def equal_op_def join_def meet_def)


[STATEMENT]
lemma BC_rel: "\<B> \<^bold>\<equiv> \<B>\<^sub>C \<C>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<B> \<^bold>\<equiv> \<B>\<^sub>C \<C>
[PROOF STEP]
by (simp add: BI_BC_rel equal_op_def)


[STATEMENT]
lemma BF_rel: "Int_2 \<I> \<Longrightarrow> \<B> \<^bold>\<equiv> \<B>\<^sub>F \<F>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<B> \<^bold>\<equiv> \<B>\<^sub>F \<F>
[PROOF STEP]
by (smt Br_fr_def Br_int_def IF_rel Int_fr_def diff_def equal_op_def meet_def)


[STATEMENT]
lemma FC_rel: "\<F> \<^bold>\<equiv> \<F>\<^sub>C \<C>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<F> \<^bold>\<equiv> \<F>\<^sub>C \<C>
[PROOF STEP]
using Fr_cl_def Fr_int_def compl_def dual_def equal_op_def meet_def
[PROOF STATE]
proof (prove)
using this:
\<F>\<^sub>C ?\<C> \<equiv> \<lambda>A. ?\<C> A \<^bold>\<and> ?\<C> (\<^bold>\<midarrow>A)
\<F>\<^sub>I ?\<I> \<equiv> ?\<I>\<^sup>c \<^bold>\<sqinter> ?\<I>\<^sup>d
\<^bold>\<midarrow>?A \<equiv> \<lambda>w. \<not> ?A w
?\<phi>\<^sup>d \<equiv> \<lambda>X. ?\<phi>\<^sup>c (\<^bold>\<midarrow>X)
?\<phi> \<^bold>\<equiv> ?\<psi> \<equiv> \<forall>X w. ?\<phi> X w = ?\<psi> X w
?A \<^bold>\<and> ?B \<equiv> \<lambda>w. ?A w \<and> ?B w

goal (1 subgoal):
 1. \<F> \<^bold>\<equiv> \<F>\<^sub>C \<C>
[PROOF STEP]
by fastforce


[STATEMENT]
lemma FB_rel: "Int_2 \<I> \<Longrightarrow> \<F> \<^bold>\<equiv> \<F>\<^sub>B \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<F> \<^bold>\<equiv> \<F>\<^sub>B \<B>
[PROOF STEP]
unfolding Fr_br_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<F> \<^bold>\<equiv> (\<lambda>A. \<B> A \<^bold>\<or> \<B> (\<^bold>\<midarrow>A))
[PROOF STEP]
by (smt BC_rel Br_cl_def CB_rel Cl_br_def FC_rel Fr_cl_def equal_op_def join_def meet_def)


[STATEMENT]
lemma fp1: "Int_2 \<I> \<Longrightarrow> \<I>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B>\<^sup>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<I>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B>\<^sup>c
[PROOF STEP]
by (smt Br_int_def IB_rel Int_br_def compl_def diff_def dimp_def equal_op_def)


[STATEMENT]
lemma fp2: "Int_2 \<I> \<Longrightarrow> \<B>\<^sup>f\<^sup>p \<^bold>\<equiv> \<I>\<^sup>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<B>\<^sup>f\<^sup>p \<^bold>\<equiv> \<I>\<^sup>c
[PROOF STEP]
using fp1
[PROOF STATE]
proof (prove)
using this:
Int_2 \<I> \<Longrightarrow> \<I>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B>\<^sup>c

goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<B>\<^sup>f\<^sup>p \<^bold>\<equiv> \<I>\<^sup>c
[PROOF STEP]
unfolding compl_def dimp_def equal_op_def
[PROOF STATE]
proof (prove)
using this:
Int_2 \<I> \<Longrightarrow> \<forall>X w. (\<I> X w = X w) = (\<not> \<B> X w)

goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<forall>X w. (\<B> X w = X w) = (\<not> \<I> X w)
[PROOF STEP]
by smt


[STATEMENT]
lemma fp3: "Int_2 \<I> \<Longrightarrow> \<C>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B>\<^sup>d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<C>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B>\<^sup>d
[PROOF STEP]
by (metis (no_types) dual_comp eq_ext' fp2 ofp_c ofp_d ofp_invol)


[STATEMENT]
lemma fp4: "Int_2 \<I> \<Longrightarrow> (\<B>\<^sup>d)\<^sup>f\<^sup>p \<^bold>\<equiv> \<C>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<B>\<^sup>d\<^sup>f\<^sup>p \<^bold>\<equiv> \<C>
[PROOF STEP]
by (smt dimp_def equal_op_def fp3)


[STATEMENT]
lemma fp5: "Int_2 \<I> \<Longrightarrow> \<F>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B> \<^bold>\<squnion> (\<C>\<^sup>c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<F>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B> \<^bold>\<squnion> \<C>\<^sup>c
[PROOF STEP]
by (smt BC_rel Br_cl_def CF_rel Cl_fr_def FI2 Fr_2_def compl_def dimp_def eq_ext' equal_op_def join_def meet_def)


[STATEMENT]
lemma Int_Open: "Int_4 \<I> \<Longrightarrow> \<forall>A. Op(\<I> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Br_6 \<I> \<Longrightarrow> \<forall>A w. \<I> (\<I> A) w = \<I> A w
[PROOF STEP]
by (simp add: IDEM_def)


[STATEMENT]
lemma Cl_Closed: "Int_4 \<I> \<Longrightarrow> \<forall>A. Cl(\<C> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Br_6 \<I> \<Longrightarrow> \<forall>A w. \<C> (\<C> A) w = \<C> A w
[PROOF STEP]
using IC4 IDEM_def
[PROOF STATE]
proof (prove)
using this:
Br_6 ?\<phi> \<Longrightarrow> Br_6 ?\<phi>\<^sup>d
Br_6 ?\<phi> \<equiv> \<forall>A w. ?\<phi> A w = ?\<phi> (?\<phi> A) w

goal (1 subgoal):
 1. Br_6 \<I> \<Longrightarrow> \<forall>A w. \<C> (\<C> A) w = \<C> A w
[PROOF STEP]
by blast


[STATEMENT]
lemma Br_Border: "Int_1a \<I> \<Longrightarrow> \<forall>A. Br(\<B> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_1a \<I> \<Longrightarrow> \<forall>A w. \<B> (\<B> A) w = \<B> A w
[PROOF STEP]
by (metis Br_int_def MONO_MULTa MONO_def diff_def)


[STATEMENT]
lemma "\<II> \<I> \<Longrightarrow> \<forall>A. Fr(\<F> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_1 \<I> \<and> Int_2 \<I> \<and> Cl_5 \<I> \<and> Br_6 \<I> \<Longrightarrow> \<forall>A w. \<F> (\<F> A) w = \<F> A w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_1 \<I> \<and> Int_2 \<I> \<and> Cl_5 \<I> \<and> Br_6 \<I> \<Longrightarrow> \<forall>A w. \<F> (\<F> A) w = \<F> A w
[PROOF STEP]
oops


[STATEMENT]
lemma OpCldual: "\<forall>A. Cl A \<longleftrightarrow> Op(\<^bold>\<midarrow>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A. (\<forall>w. \<C> A w = A w) = (\<forall>w. \<I> (\<^bold>\<midarrow>A) w = (\<^bold>\<midarrow>A) w)
[PROOF STEP]
by (simp add: fp_d)


[STATEMENT]
lemma ClOpdual: "\<forall>A. Op A \<longleftrightarrow> Cl(\<^bold>\<midarrow>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A. (\<forall>w. \<I> A w = A w) = (\<forall>w. \<C> (\<^bold>\<midarrow>A) w = (\<^bold>\<midarrow>A) w)
[PROOF STEP]
by (simp add: compl_def dual_def)


[STATEMENT]
lemma Fr_ClBr: "Int_2 \<I> \<Longrightarrow> \<forall>A. Fr(A) = (Cl(A) \<and> Br(A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<forall>A. (\<forall>w. \<F> A w = A w) = ((\<forall>w. \<C> A w = A w) \<and> (\<forall>w. \<B> A w = A w))
[PROOF STEP]
using BF_rel Br_fr_def CF_rel Cl_fr_def eq_ext' join_def meet_def
[PROOF STATE]
proof (prove)
using this:
Int_2 \<I> \<Longrightarrow> \<B> \<^bold>\<equiv> \<B>\<^sub>F \<F>
\<B>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<and> ?\<F> A
Int_2 \<I> \<Longrightarrow> \<C> \<^bold>\<equiv> \<C>\<^sub>F \<F>
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
?a \<^bold>\<equiv> ?b \<Longrightarrow> ?a = ?b
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w
?A \<^bold>\<and> ?B \<equiv> \<lambda>w. ?A w \<and> ?B w

goal (1 subgoal):
 1. Int_2 \<I> \<Longrightarrow> \<forall>A. (\<forall>w. \<F> A w = A w) = ((\<forall>w. \<C> A w = A w) \<and> (\<forall>w. \<B> A w = A w))
[PROOF STEP]
by fastforce


[STATEMENT]
lemma Cl_F: "Int_1a \<I> \<Longrightarrow> Int_2 \<I> \<Longrightarrow> Int_4 \<I> \<Longrightarrow> \<forall>A. Cl(\<F> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Int_1a \<I>; Int_2 \<I>; Br_6 \<I>\<rbrakk> \<Longrightarrow> \<forall>A w. \<C> (\<F> A) w = \<F> A w
[PROOF STEP]
by (metis CF_rel Cl_fr_def FI4 Fr_4_def eq_ext' join_def)


[STATEMENT]
lemma takeW_singleton:
  "takeW info [x] xo = (if P info x xo then [x] else [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. takeW info [x] xo = (if P info x xo then [x] else [])
[PROOF STEP]
by (simp)


[STATEMENT]
lemma takeW_two_or_more:
  "takeW info (x # y # zs) xo = (if P info x (Some y) then x # takeW (upd info y) (y # zs) xo else [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. takeW info (x # y # zs) xo = (if P info x (Some y) then x # takeW (upd info y) (y # zs) xo else [])
[PROOF STEP]
by (simp)


[STATEMENT]
lemma takeW_split_tail:
  "takeW info (x # xs) nxt =
     (if xs = []
      then (if P info x nxt then [x] else [])
      else (if P info x (Some (hd xs)) then x # takeW (upd info (hd xs)) xs nxt else []))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. takeW info (x # xs) nxt = (if xs = [] then if P info x nxt then [x] else [] else if P info x (Some (hd xs)) then x # takeW (upd info (hd xs)) xs nxt else [])
[PROOF STEP]
by (cases xs, auto)


[STATEMENT]
lemma extract_split_tail:
  "extract info (x # xs) nxt =
     (case xs of
          [] \<Rightarrow> (if P info x nxt then nxt else (Some x))
        | (y # ys) \<Rightarrow> (if P info x (Some y) then extract (upd info y) (y # ys) nxt else Some x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extract info (x # xs) nxt = (case xs of [] \<Rightarrow> if P info x nxt then nxt else Some x | y # ys \<Rightarrow> if P info x (Some y) then extract (upd info y) (y # ys) nxt else Some x)
[PROOF STEP]
by (cases xs, auto)


[STATEMENT]
lemma holds_split_tail:
  "holds info (x # xs) nxt \<longleftrightarrow>
      (case xs of
          [] \<Rightarrow> P info x nxt
        | (y # ys) \<Rightarrow> P info x (Some y) \<and> holds (upd info y) (y # ys) nxt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. holds info (x # xs) nxt = (case xs of [] \<Rightarrow> P info x nxt | y # ys \<Rightarrow> P info x (Some y) \<and> holds (upd info y) (y # ys) nxt)
[PROOF STEP]
by (cases xs, auto)


[STATEMENT]
lemma holds_Cons_P:
  "holds info (x # xs) nxt \<Longrightarrow> \<exists>y . P info x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. holds info (x # xs) nxt \<Longrightarrow> \<exists>y. P info x y
[PROOF STEP]
by (cases xs, auto)


[STATEMENT]
lemma holds_Cons_holds:
  "holds info (x # xs) nxt \<Longrightarrow> holds (upd_opt info (head xs)) xs nxt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. holds info (x # xs) nxt \<Longrightarrow> holds (upd_opt info (head xs)) xs nxt
[PROOF STEP]
by (cases xs, auto)


[STATEMENT]
lemma holds_takeW_extract: "holds info (takeW info xs nxt) (extract info xs nxt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. holds info (takeW info xs nxt) (extract info xs nxt)
[PROOF STEP]
apply(induction info xs nxt rule: takeW.induct)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>uu_ uv_. holds uu_ (takeW uu_ [] uv_) (extract uu_ [] uv_)
 2. \<And>info x xo. P info x xo \<Longrightarrow> holds info (takeW info [x] xo) (extract info [x] xo)
 3. \<And>info x xo. \<not> P info x xo \<Longrightarrow> holds info (takeW info [x] xo) (extract info [x] xo)
 4. \<And>info x y xs xo. \<lbrakk>P info x (Some y); holds (upd info y) (takeW (upd info y) (y # xs) xo) (extract (upd info y) (y # xs) xo)\<rbrakk> \<Longrightarrow> holds info (takeW info (x # y # xs) xo) (extract info (x # y # xs) xo)
 5. \<And>info x y xs xo. \<not> P info x (Some y) \<Longrightarrow> holds info (takeW info (x # y # xs) xo) (extract info (x # y # xs) xo)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>info x y xs xo. \<lbrakk>P info x (Some y); holds (upd info y) (takeW (upd info y) (y # xs) xo) (extract (upd info y) (y # xs) xo)\<rbrakk> \<Longrightarrow> holds info (x # takeW (upd info y) (y # xs) xo) (extract (upd info y) (y # xs) xo)
[PROOF STEP]
subgoal for info x y ys
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P info x (Some y); holds (upd info y) (takeW (upd info y) (y # ys) xo_) (extract (upd info y) (y # ys) xo_)\<rbrakk> \<Longrightarrow> holds info (x # takeW (upd info y) (y # ys) xo_) (extract (upd info y) (y # ys) xo_)
[PROOF STEP]
apply(cases "ys")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P info x (Some y); holds (upd info y) (takeW (upd info y) (y # ys) xo_) (extract (upd info y) (y # ys) xo_); ys = []\<rbrakk> \<Longrightarrow> holds info (x # takeW (upd info y) (y # ys) xo_) (extract (upd info y) (y # ys) xo_)
 2. \<And>a list. \<lbrakk>P info x (Some y); holds (upd info y) (takeW (upd info y) (y # ys) xo_) (extract (upd info y) (y # ys) xo_); ys = a # list\<rbrakk> \<Longrightarrow> holds info (x # takeW (upd info y) (y # ys) xo_) (extract (upd info y) (y # ys) xo_)
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma holds_append:
  "holds info (xs @ ys) nxt =
   (case ys of [] \<Rightarrow> holds info xs nxt | x # _ \<Rightarrow>
     holds info xs (Some x) \<and>
     (case xs of [] \<Rightarrow> holds info ys nxt
                | _ \<Rightarrow> holds (upds info (tl xs@[x])) ys nxt))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. holds info (xs @ ys) nxt = (case ys of [] \<Rightarrow> holds info xs nxt | x # xa \<Rightarrow> holds info xs (Some x) \<and> (case xs of [] \<Rightarrow> holds info ys nxt | a # list \<Rightarrow> holds (upds info (tl xs @ [x])) ys nxt))
[PROOF STEP]
by(induction info xs nxt rule: takeW.induct)
    (auto split: list.split)


[STATEMENT]
lemma upds_snoc: "upds uinfo (xs@[x]) = upd (upds uinfo xs) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upds uinfo (xs @ [x]) = upd (upds uinfo xs) x
[PROOF STEP]
by simp


[STATEMENT]
lemma takeW_prefix:
  "prefix (takeW info l nxt) l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix (takeW info l nxt) l
[PROOF STEP]
by (induction info l nxt rule: takeW.induct) auto


[STATEMENT]
lemma takeW_set: "t \<in> set (TWu.takeW P upd info l nxt) \<Longrightarrow> t \<in> set l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> set (takeW info l nxt) \<Longrightarrow> t \<in> set l
[PROOF STEP]
by(auto intro: takeW_prefix elim: set_prefix)


[STATEMENT]
lemma holds_implies_takeW_is_identity:
  "holds info l nxt \<Longrightarrow> takeW info l nxt = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. holds info l nxt \<Longrightarrow> takeW info l nxt = l
[PROOF STEP]
by (induction info l nxt rule: takeW.induct) auto


[STATEMENT]
lemma holds_takeW_is_identity[simp]:
  "takeW info l nxt = l \<longleftrightarrow> holds info l nxt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (takeW info l nxt = l) = holds info l nxt
[PROOF STEP]
by (induction info l nxt rule: takeW.induct) auto


[STATEMENT]
lemma takeW_takeW_extract:
  "takeW info (takeW info l nxt) (extract info l nxt)
 = takeW info l nxt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. takeW info (takeW info l nxt) (extract info l nxt) = takeW info l nxt
[PROOF STEP]
using holds_takeW_extract holds_implies_takeW_is_identity
[PROOF STATE]
proof (prove)
using this:
holds ?info (takeW ?info ?xs ?nxt) (extract ?info ?xs ?nxt)
holds ?info ?l ?nxt \<Longrightarrow> takeW ?info ?l ?nxt = ?l

goal (1 subgoal):
 1. takeW info (takeW info l nxt) (extract info l nxt) = takeW info l nxt
[PROOF STEP]
by blast


[STATEMENT]
lemma holds_set_list: "\<lbrakk>holds info l nxt; x \<in> set l\<rbrakk> \<Longrightarrow> \<exists> p y . P p x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds info l nxt; x \<in> set l\<rbrakk> \<Longrightarrow> \<exists>p y. P p x y
[PROOF STEP]
apply(induction info l nxt rule: TWu.takeW.induct[where ?Pa="P"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>uu_ uv_. \<lbrakk>holds uu_ [] uv_; x \<in> set []\<rbrakk> \<Longrightarrow> \<exists>p. Ex (P p x)
 2. \<And>info xa xo. \<lbrakk>P info xa xo; holds info [xa] xo; x \<in> set [xa]\<rbrakk> \<Longrightarrow> \<exists>p. Ex (P p x)
 3. \<And>info xa xo. \<lbrakk>\<not> P info xa xo; holds info [xa] xo; x \<in> set [xa]\<rbrakk> \<Longrightarrow> \<exists>p. Ex (P p x)
 4. \<And>info xa y xs xo. \<lbrakk>P info xa (Some y); \<lbrakk>holds (?upd info y) (y # xs) xo; x \<in> set (y # xs)\<rbrakk> \<Longrightarrow> \<exists>p. Ex (P p x); holds info (xa # y # xs) xo; x \<in> set (xa # y # xs)\<rbrakk> \<Longrightarrow> \<exists>p. Ex (P p x)
 5. \<And>info xa y xs xo. \<lbrakk>\<not> P info xa (Some y); holds info (xa # y # xs) xo; x \<in> set (xa # y # xs)\<rbrakk> \<Longrightarrow> \<exists>p. Ex (P p x)
[PROOF STEP]
by auto


[STATEMENT]
lemma holds_set_list_no_update: "\<lbrakk>holds info l nxt; x \<in> set l; \<And>a b. upd a b = a\<rbrakk> \<Longrightarrow> \<exists> y . P info x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds info l nxt; x \<in> set l; \<And>a b. upd a b = a\<rbrakk> \<Longrightarrow> \<exists>y. P info x y
[PROOF STEP]
apply(induction info l nxt rule: TWu.takeW.induct[where ?Pa="P"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>uu_ uv_. \<lbrakk>holds uu_ [] uv_; x \<in> set []; \<And>a b. upd a b = a\<rbrakk> \<Longrightarrow> Ex (P uu_ x)
 2. \<And>info xa xo. \<lbrakk>P info xa xo; holds info [xa] xo; x \<in> set [xa]; \<And>a b. upd a b = a\<rbrakk> \<Longrightarrow> Ex (P info x)
 3. \<And>info xa xo. \<lbrakk>\<not> P info xa xo; holds info [xa] xo; x \<in> set [xa]; \<And>a b. upd a b = a\<rbrakk> \<Longrightarrow> Ex (P info x)
 4. \<And>info xa y xs xo. \<lbrakk>P info xa (Some y); \<lbrakk>holds (?upd info y) (y # xs) xo; x \<in> set (y # xs); \<And>a b. upd a b = a\<rbrakk> \<Longrightarrow> Ex (P (?upd info y) x); holds info (xa # y # xs) xo; x \<in> set (xa # y # xs); \<And>a b. upd a b = a\<rbrakk> \<Longrightarrow> Ex (P info x)
 5. \<And>info xa y xs xo. \<lbrakk>\<not> P info xa (Some y); holds info (xa # y # xs) xo; x \<in> set (xa # y # xs); \<And>a b. upd a b = a\<rbrakk> \<Longrightarrow> Ex (P info x)
[PROOF STEP]
by auto


[STATEMENT]
lemma holds_unfold: "holds info l None \<Longrightarrow>
  l = [] \<or>
  (\<exists> x . l = [x] \<and> P info x None) \<or>
  (\<exists> x y ys . l = (x#y#ys) \<and> P info x (Some y) \<and> holds (upd info y) (y#ys) None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. holds info l None \<Longrightarrow> l = [] \<or> (\<exists>x. l = [x] \<and> P info x None) \<or> (\<exists>x y ys. l = x # y # ys \<and> P info x (Some y) \<and> holds (upd info y) (y # ys) None)
[PROOF STEP]
by auto (meson holds.elims(2))


[STATEMENT]
lemma holds_unfold_prexnxt': (*weakened!*)
  "\<lbrakk>holds info l nxt; l = (zs@(x1#x2#xs)); zs \<noteq> []\<rbrakk>
 \<Longrightarrow> P (upds info ((tl zs)@[x1])) x1 (Some x2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds info l nxt; l = zs @ x1 # x2 # xs; zs \<noteq> []\<rbrakk> \<Longrightarrow> P (upds info (tl zs @ [x1])) x1 (Some x2)
[PROOF STEP]
apply(cases zs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>holds info l nxt; l = zs @ x1 # x2 # xs; zs \<noteq> []; zs = []\<rbrakk> \<Longrightarrow> P (upds info (tl zs @ [x1])) x1 (Some x2)
 2. \<And>a list. \<lbrakk>holds info l nxt; l = zs @ x1 # x2 # xs; zs \<noteq> []; zs = a # list\<rbrakk> \<Longrightarrow> P (upds info (tl zs @ [x1])) x1 (Some x2)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>holds info l nxt; l = zs @ x1 # x2 # xs; zs \<noteq> []; zs = a # list\<rbrakk> \<Longrightarrow> P (upds info (tl zs @ [x1])) x1 (Some x2)
[PROOF STEP]
apply(simp only: TWu.holds_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>case x1 # x2 # xs of [] \<Rightarrow> holds info (a # list) nxt | x # xa \<Rightarrow> holds info (a # list) (Some x) \<and> (case a # list of [] \<Rightarrow> holds info (x1 # x2 # xs) nxt | aa # lista \<Rightarrow> holds (upds info (tl (a # list) @ [x])) (x1 # x2 # xs) nxt); l = (a # list) @ x1 # x2 # xs; a # list \<noteq> []; zs = a # list\<rbrakk> \<Longrightarrow> P (upds info (tl (a # list) @ [x1])) x1 (Some x2)
[PROOF STEP]
by auto


[STATEMENT]
lemma holds_suffix:
  "\<lbrakk>holds info l nxt; suffix l' l\<rbrakk> \<Longrightarrow> \<exists> info'. holds info' l' nxt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds info l nxt; suffix l' l\<rbrakk> \<Longrightarrow> \<exists>info'. holds info' l' nxt
[PROOF STEP]
apply(cases l')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>holds info l nxt; suffix l' l; l' = []\<rbrakk> \<Longrightarrow> \<exists>info'. holds info' l' nxt
 2. \<And>a list. \<lbrakk>holds info l nxt; suffix l' l; l' = a # list\<rbrakk> \<Longrightarrow> \<exists>info'. holds info' l' nxt
[PROOF STEP]
by(auto simp add: suffix_def TWu.holds_append list.case_eq_if)


[STATEMENT]
lemma holds_unfold_prelnil:
  "\<lbrakk>holds info l nxt; l = (zs@(x1#[])); zs \<noteq> []\<rbrakk>
 \<Longrightarrow> P (upds info ((tl zs)@[x1])) x1 nxt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds info l nxt; l = zs @ [x1]; zs \<noteq> []\<rbrakk> \<Longrightarrow> P (upds info (tl zs @ [x1])) x1 nxt
[PROOF STEP]
apply(cases zs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>holds info l nxt; l = zs @ [x1]; zs \<noteq> []; zs = []\<rbrakk> \<Longrightarrow> P (upds info (tl zs @ [x1])) x1 nxt
 2. \<And>a list. \<lbrakk>holds info l nxt; l = zs @ [x1]; zs \<noteq> []; zs = a # list\<rbrakk> \<Longrightarrow> P (upds info (tl zs @ [x1])) x1 nxt
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>holds info l nxt; l = zs @ [x1]; zs \<noteq> []; zs = []\<rbrakk> \<Longrightarrow> P (upds info (tl zs @ [x1])) x1 nxt
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>holds info l nxt; l = zs @ [x1]; zs \<noteq> []; zs = a # list\<rbrakk> \<Longrightarrow> P (upds info (tl zs @ [x1])) x1 nxt
[PROOF STEP]
by(simp only: TWu.holds_append) auto


[STATEMENT]
lemma holds_intermediate:
  assumes "holds uinfo p nxt" "p = pre @ hf # post"
  shows "holds (upd_shifted uinfo pre hf) (hf # post) nxt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. holds (upd_shifted uinfo pre hf) (hf # post) nxt
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
holds uinfo p nxt
p = pre @ hf # post

goal (1 subgoal):
 1. holds (upd_shifted uinfo pre hf) (hf # post) nxt
[PROOF STEP]
proof(induction pre arbitrary: p uinfo hf)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p uinfo hf. \<lbrakk>holds uinfo p nxt; p = [] @ hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted uinfo [] hf) (hf # post) nxt
 2. \<And>a pre p uinfo hf. \<lbrakk>\<And>p uinfo hf. \<lbrakk>holds uinfo p nxt; p = pre @ hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted uinfo pre hf) (hf # post) nxt; holds uinfo p nxt; p = (a # pre) @ hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted uinfo (a # pre) hf) (hf # post) nxt
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
holds uinfo p nxt
p = [] @ hf # post

goal (2 subgoals):
 1. \<And>p uinfo hf. \<lbrakk>holds uinfo p nxt; p = [] @ hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted uinfo [] hf) (hf # post) nxt
 2. \<And>a pre p uinfo hf. \<lbrakk>\<And>p uinfo hf. \<lbrakk>holds uinfo p nxt; p = pre @ hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted uinfo pre hf) (hf # post) nxt; holds uinfo p nxt; p = (a # pre) @ hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted uinfo (a # pre) hf) (hf # post) nxt
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
holds uinfo p nxt
p = [] @ hf # post
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
holds uinfo p nxt
p = [] @ hf # post

goal (1 subgoal):
 1. holds (upd_shifted uinfo [] hf) (hf # post) nxt
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
holds uinfo p nxt
p = [] @ hf # post
holds uinfo p nxt
p = pre @ hf # post

goal (1 subgoal):
 1. holds (upd_shifted uinfo [] hf) (hf # post) nxt
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
holds (upd_shifted uinfo [] hf) (hf # post) nxt

goal (1 subgoal):
 1. \<And>a pre p uinfo hf. \<lbrakk>\<And>p uinfo hf. \<lbrakk>holds uinfo p nxt; p = pre @ hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted uinfo pre hf) (hf # post) nxt; holds uinfo p nxt; p = (a # pre) @ hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted uinfo (a # pre) hf) (hf # post) nxt
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a pre p uinfo hf. \<lbrakk>\<And>p uinfo hf. \<lbrakk>holds uinfo p nxt; p = pre @ hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted uinfo pre hf) (hf # post) nxt; holds uinfo p nxt; p = (a # pre) @ hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted uinfo (a # pre) hf) (hf # post) nxt
[PROOF STEP]
case induct_asm: (Cons a prev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>holds ?uinfo ?p nxt; ?p = prev @ ?hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted ?uinfo prev ?hf) (?hf # post) nxt
holds uinfo p nxt
p = (a # prev) @ hf # post

goal (1 subgoal):
 1. \<And>a pre p uinfo hf. \<lbrakk>\<And>p uinfo hf. \<lbrakk>holds uinfo p nxt; p = pre @ hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted uinfo pre hf) (hf # post) nxt; holds uinfo p nxt; p = (a # pre) @ hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted uinfo (a # pre) hf) (hf # post) nxt
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt
[PROOF STEP]
proof(cases prev)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. prev = [] \<Longrightarrow> holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt
 2. \<And>aa list. prev = aa # list \<Longrightarrow> holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
prev = []

goal (2 subgoals):
 1. prev = [] \<Longrightarrow> holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt
 2. \<And>aa list. prev = aa # list \<Longrightarrow> holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prev = []
[PROOF STEP]
have "holds (upd uinfo hf) (hf # post) nxt"
[PROOF STATE]
proof (prove)
using this:
prev = []

goal (1 subgoal):
 1. holds (upd uinfo hf) (hf # post) nxt
[PROOF STEP]
using induct_asm
[PROOF STATE]
proof (prove)
using this:
prev = []
\<lbrakk>holds ?uinfo ?p nxt; ?p = prev @ ?hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted ?uinfo prev ?hf) (?hf # post) nxt
holds uinfo p nxt
p = (a # prev) @ hf # post

goal (1 subgoal):
 1. holds (upd uinfo hf) (hf # post) nxt
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
holds (upd uinfo hf) (hf # post) nxt

goal (2 subgoals):
 1. prev = [] \<Longrightarrow> holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt
 2. \<And>aa list. prev = aa # list \<Longrightarrow> holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
holds (upd uinfo hf) (hf # post) nxt
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
holds (upd uinfo hf) (hf # post) nxt

goal (1 subgoal):
 1. holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt
[PROOF STEP]
using induct_asm Nil
[PROOF STATE]
proof (prove)
using this:
holds (upd uinfo hf) (hf # post) nxt
\<lbrakk>holds ?uinfo ?p nxt; ?p = prev @ ?hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted ?uinfo prev ?hf) (?hf # post) nxt
holds uinfo p nxt
p = (a # prev) @ hf # post
prev = []

goal (1 subgoal):
 1. holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt

goal (1 subgoal):
 1. \<And>aa list. prev = aa # list \<Longrightarrow> holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. prev = aa # list \<Longrightarrow> holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt
[PROOF STEP]
case cons_asm: (Cons b list)
[PROOF STATE]
proof (state)
this:
prev = b # list

goal (1 subgoal):
 1. \<And>aa list. prev = aa # list \<Longrightarrow> holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prev = b # list
[PROOF STEP]
have "holds (upd uinfo b) (b # list @ hf # post) nxt"
[PROOF STATE]
proof (prove)
using this:
prev = b # list

goal (1 subgoal):
 1. holds (upd uinfo b) (b # list @ hf # post) nxt
[PROOF STEP]
using induct_asm(2-3)
[PROOF STATE]
proof (prove)
using this:
prev = b # list
holds uinfo p nxt
p = (a # prev) @ hf # post

goal (1 subgoal):
 1. holds (upd uinfo b) (b # list @ hf # post) nxt
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
holds (upd uinfo b) (b # list @ hf # post) nxt

goal (1 subgoal):
 1. \<And>aa list. prev = aa # list \<Longrightarrow> holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
holds (upd uinfo b) (b # list @ hf # post) nxt
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
holds (upd uinfo b) (b # list @ hf # post) nxt

goal (1 subgoal):
 1. holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt
[PROOF STEP]
using induct_asm(1)
[PROOF STATE]
proof (prove)
using this:
holds (upd uinfo b) (b # list @ hf # post) nxt
\<lbrakk>holds ?uinfo ?p nxt; ?p = prev @ ?hf # post\<rbrakk> \<Longrightarrow> holds (upd_shifted ?uinfo prev ?hf) (?hf # post) nxt

goal (1 subgoal):
 1. holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt
[PROOF STEP]
by (simp add: cons_asm)
[PROOF STATE]
proof (state)
this:
holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
holds (upd_shifted uinfo (a # prev) hf) (hf # post) nxt

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma holds_intermediate_ex:
  assumes "holds uinfo hfs nxt" "hf \<in> set hfs"
  shows "\<exists>pre post . holds (upd_shifted uinfo pre hf) (hf # post) nxt \<and> hfs = pre @ hf # post"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pre post. holds (upd_shifted uinfo pre hf) (hf # post) nxt \<and> hfs = pre @ hf # post
[PROOF STEP]
using assms holds_intermediate
[PROOF STATE]
proof (prove)
using this:
holds uinfo hfs nxt
hf \<in> set hfs
\<lbrakk>holds ?uinfo ?p ?nxt; ?p = ?pre @ ?hf # ?post\<rbrakk> \<Longrightarrow> holds (upd_shifted ?uinfo ?pre ?hf) (?hf # ?post) ?nxt

goal (1 subgoal):
 1. \<exists>pre post. holds (upd_shifted uinfo pre hf) (hf # post) nxt \<and> hfs = pre @ hf # post
[PROOF STEP]
by (meson split_list)


[STATEMENT]
lemma alignUp_unfold:
  \<open>alignUp w n = (w + mask n) AND NOT (mask n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alignUp w n = w + mask n AND NOT (mask n)
[PROOF STEP]
by (simp add: alignUp_def mask_eq_exp_minus_1 add_mask_fold)


[STATEMENT]
lemma word_ctz_unfold:
  \<open>word_ctz w = length (takeWhile (Not \<circ> bit w) [0..<LENGTH('a)])\<close> for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_ctz w = length (takeWhile (Not \<circ> bit w) [0..<LENGTH('a)])
[PROOF STEP]
by (simp add: word_ctz_def rev_to_bl_eq takeWhile_map)