[STATEMENT]
lemma StarLR_Times_Plus_One[simp]: "StarLR (Times r (Plus One s)) s = StarLR r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. StarLR (Times r (Plus One s)) s = StarLR r s
[PROOF STEP]
proof (coinduction arbitrary: r s)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r s. \<oo> (StarLR (Times r (Plus One s)) s) = \<oo> (StarLR r s) \<and> (\<forall>x. (\<exists>ra sa. \<dd> (StarLR (Times r (Plus One s)) s) x = StarLR (Times ra (Plus One sa)) sa \<and> \<dd> (StarLR r s) x = StarLR ra sa) \<or> \<dd> (StarLR (Times r (Plus One s)) s) x = \<dd> (StarLR r s) x)
[PROOF STEP]
case Lang
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>r s. \<oo> (StarLR (Times r (Plus One s)) s) = \<oo> (StarLR r s) \<and> (\<forall>x. (\<exists>ra sa. \<dd> (StarLR (Times r (Plus One s)) s) x = StarLR (Times ra (Plus One sa)) sa \<and> \<dd> (StarLR r s) x = StarLR ra sa) \<or> \<dd> (StarLR (Times r (Plus One s)) s) x = \<dd> (StarLR r s) x)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>r s. \<oo> (StarLR (Times r (Plus One s)) s) = \<oo> (StarLR r s) \<and> (\<forall>x. (\<exists>ra sa. \<dd> (StarLR (Times r (Plus One s)) s) x = StarLR (Times ra (Plus One sa)) sa \<and> \<dd> (StarLR r s) x = StarLR ra sa) \<or> \<dd> (StarLR (Times r (Plus One s)) s) x = \<dd> (StarLR r s) x)
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r s. \<oo> (StarLR (Times r (Plus One s)) s) = \<oo> (StarLR r s) \<and> (\<forall>x. (\<exists>ra sa. \<dd> (StarLR (Times r (Plus One s)) s) x = StarLR (Times ra (Plus One sa)) sa \<and> \<dd> (StarLR r s) x = StarLR ra sa) \<or> \<dd> (StarLR (Times r (Plus One s)) s) x = \<dd> (StarLR r s) x)
[PROOF STEP]
define L and R where "L = Plus (\<dd> r a) (Plus (Times (\<dd> r a) s) (\<dd> s a))"
    and "R = Times (Plus (\<dd> r a) (Plus (Times (\<dd> r a) s) (\<dd> s a))) s"
[PROOF STATE]
proof (state)
this:
L = Plus (\<dd> r a) (Plus (Times (\<dd> r a) s) (\<dd> s a))
R = Times (Plus (\<dd> r a) (Plus (Times (\<dd> r a) s) (\<dd> s a))) s

goal (1 subgoal):
 1. \<And>r s. \<oo> (StarLR (Times r (Plus One s)) s) = \<oo> (StarLR r s) \<and> (\<forall>x. (\<exists>ra sa. \<dd> (StarLR (Times r (Plus One s)) s) x = StarLR (Times ra (Plus One sa)) sa \<and> \<dd> (StarLR r s) x = StarLR ra sa) \<or> \<dd> (StarLR (Times r (Plus One s)) s) x = \<dd> (StarLR r s) x)
[PROOF STEP]
have "Plus L (Plus R (\<dd> s a)) = Plus (Plus L (\<dd> s a)) R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus L (Plus R (\<dd> s a)) = Plus (Plus L (\<dd> s a)) R
[PROOF STEP]
by (metis Plus_assoc Plus_comm)
[PROOF STATE]
proof (state)
this:
Plus L (Plus R (\<dd> s a)) = Plus (Plus L (\<dd> s a)) R

goal (1 subgoal):
 1. \<And>r s. \<oo> (StarLR (Times r (Plus One s)) s) = \<oo> (StarLR r s) \<and> (\<forall>x. (\<exists>ra sa. \<dd> (StarLR (Times r (Plus One s)) s) x = StarLR (Times ra (Plus One sa)) sa \<and> \<dd> (StarLR r s) x = StarLR ra sa) \<or> \<dd> (StarLR (Times r (Plus One s)) s) x = \<dd> (StarLR r s) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Plus L (Plus R (\<dd> s a)) = Plus (Plus L (\<dd> s a)) R

goal (1 subgoal):
 1. \<And>r s. \<oo> (StarLR (Times r (Plus One s)) s) = \<oo> (StarLR r s) \<and> (\<forall>x. (\<exists>ra sa. \<dd> (StarLR (Times r (Plus One s)) s) x = StarLR (Times ra (Plus One sa)) sa \<and> \<dd> (StarLR r s) x = StarLR ra sa) \<or> \<dd> (StarLR (Times r (Plus One s)) s) x = \<dd> (StarLR r s) x)
[PROOF STEP]
have "Plus L (\<dd> s a) = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus L (\<dd> s a) = L
[PROOF STEP]
unfolding L_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus (Plus (\<dd> r a) (Plus (Times (\<dd> r a) s) (\<dd> s a))) (\<dd> s a) = Plus (\<dd> r a) (Plus (Times (\<dd> r a) s) (\<dd> s a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Plus L (\<dd> s a) = L

goal (1 subgoal):
 1. \<And>r s. \<oo> (StarLR (Times r (Plus One s)) s) = \<oo> (StarLR r s) \<and> (\<forall>x. (\<exists>ra sa. \<dd> (StarLR (Times r (Plus One s)) s) x = StarLR (Times ra (Plus One sa)) sa \<and> \<dd> (StarLR r s) x = StarLR ra sa) \<or> \<dd> (StarLR (Times r (Plus One s)) s) x = \<dd> (StarLR r s) x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Plus L (Plus R (\<dd> s a)) = Plus L R
[PROOF STEP]
have "Plus L (Plus R (\<dd> s a)) = Plus L R"
[PROOF STATE]
proof (prove)
using this:
Plus L (Plus R (\<dd> s a)) = Plus L R

goal (1 subgoal):
 1. Plus L (Plus R (\<dd> s a)) = Plus L R
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Plus L (Plus R (\<dd> s a)) = Plus L R

goal (1 subgoal):
 1. \<And>r s. \<oo> (StarLR (Times r (Plus One s)) s) = \<oo> (StarLR r s) \<and> (\<forall>x. (\<exists>ra sa. \<dd> (StarLR (Times r (Plus One s)) s) x = StarLR (Times ra (Plus One sa)) sa \<and> \<dd> (StarLR r s) x = StarLR ra sa) \<or> \<dd> (StarLR (Times r (Plus One s)) s) x = \<dd> (StarLR r s) x)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Plus (Plus (\<dd> r ?a2) (Plus (Times (\<dd> r ?a2) s) (\<dd> s ?a2))) (Plus (Times (Plus (\<dd> r ?a2) (Plus (Times (\<dd> r ?a2) s) (\<dd> s ?a2))) s) (\<dd> s ?a2)) = Plus (Plus (\<dd> r ?a2) (Plus (Times (\<dd> r ?a2) s) (\<dd> s ?a2))) (Times (Plus (\<dd> r ?a2) (Plus (Times (\<dd> r ?a2) s) (\<dd> s ?a2))) s)

goal (1 subgoal):
 1. \<And>r s. \<oo> (StarLR (Times r (Plus One s)) s) = \<oo> (StarLR r s) \<and> (\<forall>x. (\<exists>ra sa. \<dd> (StarLR (Times r (Plus One s)) s) x = StarLR (Times ra (Plus One sa)) sa \<and> \<dd> (StarLR r s) x = StarLR ra sa) \<or> \<dd> (StarLR (Times r (Plus One s)) s) x = \<dd> (StarLR r s) x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plus (Plus (\<dd> r ?a2) (Plus (Times (\<dd> r ?a2) s) (\<dd> s ?a2))) (Plus (Times (Plus (\<dd> r ?a2) (Plus (Times (\<dd> r ?a2) s) (\<dd> s ?a2))) s) (\<dd> s ?a2)) = Plus (Plus (\<dd> r ?a2) (Plus (Times (\<dd> r ?a2) s) (\<dd> s ?a2))) (Times (Plus (\<dd> r ?a2) (Plus (Times (\<dd> r ?a2) s) (\<dd> s ?a2))) s)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Plus (Plus (\<dd> r ?a2) (Plus (Times (\<dd> r ?a2) s) (\<dd> s ?a2))) (Plus (Times (Plus (\<dd> r ?a2) (Plus (Times (\<dd> r ?a2) s) (\<dd> s ?a2))) s) (\<dd> s ?a2)) = Plus (Plus (\<dd> r ?a2) (Plus (Times (\<dd> r ?a2) s) (\<dd> s ?a2))) (Times (Plus (\<dd> r ?a2) (Plus (Times (\<dd> r ?a2) s) (\<dd> s ?a2))) s)

goal (1 subgoal):
 1. \<oo> (StarLR (Times r (Plus One s)) s) = \<oo> (StarLR r s) \<and> (\<forall>x. (\<exists>r s. \<dd> (StarLR (Times r (Plus One s)) s) x = StarLR (Times r (Plus One s)) s \<and> \<dd> (StarLR r s) x = StarLR r s) \<or> \<dd> (StarLR (Times r (Plus One s)) s) x = \<dd> (StarLR r s) x)
[PROOF STEP]
by (auto simp del: StarLR_Plus Plus_assoc Times_PlusL)
[PROOF STATE]
proof (state)
this:
\<oo> (StarLR (Times r (Plus One s)) s) = \<oo> (StarLR r s) \<and> (\<forall>x. (\<exists>r s. \<dd> (StarLR (Times r (Plus One s)) s) x = StarLR (Times r (Plus One s)) s \<and> \<dd> (StarLR r s) x = StarLR r s) \<or> \<dd> (StarLR (Times r (Plus One s)) s) x = \<dd> (StarLR r s) x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma StarLR_Times: "StarLR (Times r s) t = Times r (StarLR s t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. StarLR (Times r s) t = Times r (StarLR s t)
[PROOF STEP]
by (coinduction arbitrary: r s t rule: language_coinduct_upto_Plus)
    (fastforce simp del: Plus_ACI Times_PlusR)


[STATEMENT]
lemma \<oo>_Star[simp]: "\<oo> (Star r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> (Star r)
[PROOF STEP]
unfolding Star_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> (StarLR One r)
[PROOF STEP]
by simp


[STATEMENT]
lemma \<dd>_Star[simp]: "\<dd> (Star r) = (\<lambda>a. Times (\<dd> r a) (Star r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dd> (Star r) = (\<lambda>a. Times (\<dd> r a) (Star r))
[PROOF STEP]
unfolding Star_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dd> (StarLR One r) = (\<lambda>a. Times (\<dd> r a) (StarLR One r))
[PROOF STEP]
by (auto simp add: Star_def StarLR_Times[symmetric])


[STATEMENT]
lemma Star_Zero[simp]: "Star Zero = One"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Star Zero = One
[PROOF STEP]
by coinduction auto


[STATEMENT]
lemma Star_One[simp]: "Star One = One"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Star One = One
[PROOF STEP]
by coinduction auto


[STATEMENT]
lemma Star_unfoldL: "Star r = Plus One (Times r (Star r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Star r = Plus One (Times r (Star r))
[PROOF STEP]
by coinduction auto


[STATEMENT]
lemma ShuffleLR_ZeroL[simp]: "ShuffleLR Zero r = Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ShuffleLR Zero r = Zero
[PROOF STEP]
by (coinduction arbitrary: r) auto


[STATEMENT]
lemma ShuffleLR_ZeroR[simp]: "ShuffleLR r Zero = Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ShuffleLR r Zero = Zero
[PROOF STEP]
by (coinduction arbitrary: r) (auto intro: exI[of _ Zero])


[STATEMENT]
lemma ShuffleLR_PlusL[simp]: "ShuffleLR (Plus r s) t = Plus (ShuffleLR r t) (ShuffleLR s t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ShuffleLR (Plus r s) t = Plus (ShuffleLR r t) (ShuffleLR s t)
[PROOF STEP]
by (coinduction arbitrary: r s t) auto


[STATEMENT]
lemma ShuffleLR_PlusR[simp]: "ShuffleLR r (Plus s t) = Plus (ShuffleLR r s) (ShuffleLR r t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ShuffleLR r (Plus s t) = Plus (ShuffleLR r s) (ShuffleLR r t)
[PROOF STEP]
by (coinduction arbitrary: r s t) auto


[STATEMENT]
lemma Shuffle_Plus_ShuffleLR_PlusL[simp]:
  "Times_Plus (ShuffleLR (Plus r s) t) = Plus (Times_Plus (ShuffleLR r t)) (Times_Plus (ShuffleLR s t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times_Plus (ShuffleLR (Plus r s) t) = Plus (Times_Plus (ShuffleLR r t)) (Times_Plus (ShuffleLR s t))
[PROOF STEP]
by (coinduction arbitrary: r s t) auto


[STATEMENT]
lemma Shuffle_Plus_ShuffleLR_PlusR[simp]:
  "Times_Plus (ShuffleLR r (Plus s t)) = Plus (Times_Plus (ShuffleLR r s)) (Times_Plus (ShuffleLR r t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times_Plus (ShuffleLR r (Plus s t)) = Plus (Times_Plus (ShuffleLR r s)) (Times_Plus (ShuffleLR r t))
[PROOF STEP]
by (coinduction arbitrary: r s t) auto


[STATEMENT]
lemma \<dd>_Shuffle[simp]:
  "\<dd> (Shuffle r s) = (\<lambda>a. Plus (Shuffle (\<dd> r a) s) (Shuffle r (\<dd> s a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dd> (Shuffle r s) = (\<lambda>a. Plus (Shuffle (\<dd> r a) s) (Shuffle r (\<dd> s a)))
[PROOF STEP]
unfolding Shuffle_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dd> (Times_Plus (ShuffleLR r s)) = (\<lambda>a. Plus (Times_Plus (ShuffleLR (\<dd> r a) s)) (Times_Plus (ShuffleLR r (\<dd> s a))))
[PROOF STEP]
by auto


[STATEMENT]
theorem Shuffle_ZeroL[simp]: "Shuffle Zero r = Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Shuffle Zero r = Zero
[PROOF STEP]
by (coinduction arbitrary: r rule: language_coinduct_upto_Plus) (auto 0 4)


[STATEMENT]
theorem Shuffle_ZeroR[simp]: "Shuffle r Zero = Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Shuffle r Zero = Zero
[PROOF STEP]
by (coinduction arbitrary: r rule: language_coinduct_upto_Plus) (auto 0 4)


[STATEMENT]
theorem Shuffle_OneL[simp]: "Shuffle One r = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Shuffle One r = r
[PROOF STEP]
by (coinduction arbitrary: r) simp


[STATEMENT]
theorem Shuffle_OneR[simp]: "Shuffle r One = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Shuffle r One = r
[PROOF STEP]
by (coinduction arbitrary: r) simp


[STATEMENT]
theorem Shuffle_PlusL[simp]: "Shuffle (Plus r s) t = Plus (Shuffle r t) (Shuffle s t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Shuffle (Plus r s) t = Plus (Shuffle r t) (Shuffle s t)
[PROOF STEP]
by (coinduction arbitrary: r s t rule: language_coinduct_upto_Plus)
    (force intro!: Trans[OF Plus[OF Base Base] Refl])


[STATEMENT]
theorem Shuffle_PlusR[simp]: "Shuffle r (Plus s t) = Plus (Shuffle r s) (Shuffle r t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Shuffle r (Plus s t) = Plus (Shuffle r s) (Shuffle r t)
[PROOF STEP]
by (coinduction arbitrary: r s t rule: language_coinduct_upto_Plus)
    (force intro!: Trans[OF Plus[OF Base Base] Refl])


[STATEMENT]
theorem Shuffle_assoc[simp]: "Shuffle (Shuffle r s) t = Shuffle r (Shuffle s t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Shuffle (Shuffle r s) t = Shuffle r (Shuffle s t)
[PROOF STEP]
by (coinduction arbitrary: r s t rule: language_coinduct_upto_Plus) fastforce


[STATEMENT]
theorem Shuffle_comm[simp]: "Shuffle r s = Shuffle s r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Shuffle r s = Shuffle s r
[PROOF STEP]
by (coinduction arbitrary: r s rule: language_coinduct_upto_Plus)
    (auto intro!: Trans[OF Plus[OF Base Base] Refl])


[STATEMENT]
lemma language_coinduct_upto_regular[unfolded rel_fun_def, simplified, case_names Lang, consumes 1]:
  assumes R: "R L K" and hyp:
    "(\<And>L K. R L K \<Longrightarrow> \<oo> L = \<oo> K \<and> rel_fun (=) (regular_cong R) (\<dd> L) (\<dd> K))"
  shows "L = K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L = K
[PROOF STEP]
proof (coinduct rule: language.coinduct[of "regular_cong R"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. regular_cong R L K
 2. \<And>language language'. regular_cong R language language' \<Longrightarrow> \<oo> language = \<oo> language' \<and> rel_fun (=) (regular_cong R) (\<dd> language) (\<dd> language')
[PROOF STEP]
fix L K
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. regular_cong R L K
 2. \<And>language language'. regular_cong R language language' \<Longrightarrow> \<oo> language = \<oo> language' \<and> rel_fun (=) (regular_cong R) (\<dd> language) (\<dd> language')
[PROOF STEP]
assume "regular_cong R L K"
[PROOF STATE]
proof (state)
this:
regular_cong R L K

goal (2 subgoals):
 1. regular_cong R L K
 2. \<And>language language'. regular_cong R language language' \<Longrightarrow> \<oo> language = \<oo> language' \<and> rel_fun (=) (regular_cong R) (\<dd> language) (\<dd> language')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
regular_cong R L K
[PROOF STEP]
show "\<oo> L = \<oo> K \<and> rel_fun (=) (regular_cong R) (\<dd> L) (\<dd> K)"
[PROOF STATE]
proof (prove)
using this:
regular_cong R L K

goal (1 subgoal):
 1. \<oo> L = \<oo> K \<and> rel_fun (=) (regular_cong R) (\<dd> L) (\<dd> K)
[PROOF STEP]
by (induct rule: regular_cong.induct) (auto dest: hyp simp: rel_fun_def)
[PROOF STATE]
proof (state)
this:
\<oo> L = \<oo> K \<and> rel_fun (=) (regular_cong R) (\<dd> L) (\<dd> K)

goal (1 subgoal):
 1. regular_cong R L K
[PROOF STEP]
qed (intro Base R)


[STATEMENT]
lemma Star_unfoldR: "Star r = Plus One (Times (Star r) r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Star r = Plus One (Times (Star r) r)
[PROOF STEP]
proof (coinduction arbitrary: r rule: language_coinduct_upto_regular)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. \<oo> (Star r) = \<oo> (Plus One (Times (Star r) r)) \<and> (\<forall>x. regular_cong (\<lambda>L__ K__. \<exists>r. L__ = Star r \<and> K__ = Plus One (Times (Star r) r)) (\<dd> (Star r) x) (\<dd> (Plus One (Times (Star r) r)) x))
[PROOF STEP]
case Lang
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>r. \<oo> (Star r) = \<oo> (Plus One (Times (Star r) r)) \<and> (\<forall>x. regular_cong (\<lambda>L__ K__. \<exists>r. L__ = Star r \<and> K__ = Plus One (Times (Star r) r)) (\<dd> (Star r) x) (\<dd> (Plus One (Times (Star r) r)) x))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>r. \<oo> (Star r) = \<oo> (Plus One (Times (Star r) r)) \<and> (\<forall>x. regular_cong (\<lambda>L__ K__. \<exists>r. L__ = Star r \<and> K__ = Plus One (Times (Star r) r)) (\<dd> (Star r) x) (\<dd> (Plus One (Times (Star r) r)) x))
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. \<oo> (Star r) = \<oo> (Plus One (Times (Star r) r)) \<and> (\<forall>x. regular_cong (\<lambda>L__ K__. \<exists>r. L__ = Star r \<and> K__ = Plus One (Times (Star r) r)) (\<dd> (Star r) x) (\<dd> (Plus One (Times (Star r) r)) x))
[PROOF STEP]
have "Plus (Times (\<dd> r a) (Times (Star r) r)) (\<dd> r a) =
      Times (\<dd> r a) (Plus One (Times (Star r) r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus (Times (\<dd> r a) (Times (Star r) r)) (\<dd> r a) = Times (\<dd> r a) (Plus One (Times (Star r) r))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Plus (Times (\<dd> r a) (Times (Star r) r)) (\<dd> r a) = Times (\<dd> r a) (Plus One (Times (Star r) r))

goal (1 subgoal):
 1. \<And>r. \<oo> (Star r) = \<oo> (Plus One (Times (Star r) r)) \<and> (\<forall>x. regular_cong (\<lambda>L__ K__. \<exists>r. L__ = Star r \<and> K__ = Plus One (Times (Star r) r)) (\<dd> (Star r) x) (\<dd> (Plus One (Times (Star r) r)) x))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Plus (Times (\<dd> r ?a2) (Times (Star r) r)) (\<dd> r ?a2) = Times (\<dd> r ?a2) (Plus One (Times (Star r) r))

goal (1 subgoal):
 1. \<And>r. \<oo> (Star r) = \<oo> (Plus One (Times (Star r) r)) \<and> (\<forall>x. regular_cong (\<lambda>L__ K__. \<exists>r. L__ = Star r \<and> K__ = Plus One (Times (Star r) r)) (\<dd> (Star r) x) (\<dd> (Plus One (Times (Star r) r)) x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plus (Times (\<dd> r ?a2) (Times (Star r) r)) (\<dd> r ?a2) = Times (\<dd> r ?a2) (Plus One (Times (Star r) r))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Plus (Times (\<dd> r ?a2) (Times (Star r) r)) (\<dd> r ?a2) = Times (\<dd> r ?a2) (Plus One (Times (Star r) r))

goal (1 subgoal):
 1. \<oo> (Star r) = \<oo> (Plus One (Times (Star r) r)) \<and> (\<forall>x. regular_cong (\<lambda>L__ K__. \<exists>r. L__ = Star r \<and> K__ = Plus One (Times (Star r) r)) (\<dd> (Star r) x) (\<dd> (Plus One (Times (Star r) r)) x))
[PROOF STEP]
by (auto simp del: Times_PlusR)
[PROOF STATE]
proof (state)
this:
\<oo> (Star r) = \<oo> (Plus One (Times (Star r) r)) \<and> (\<forall>x. regular_cong (\<lambda>L__ K__. \<exists>r. L__ = Star r \<and> K__ = Plus One (Times (Star r) r)) (\<dd> (Star r) x) (\<dd> (Plus One (Times (Star r) r)) x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Star_Star[simp]: "Star (Star r) = Star r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Star (Star r) = Star r
[PROOF STEP]
by (subst Star_unfoldL, coinduction arbitrary: r rule: language_coinduct_upto_regular) auto


[STATEMENT]
lemma Times_Star[simp]: "Times (Star r) (Star r) = Star r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times (Star r) (Star r) = Star r
[PROOF STEP]
proof (coinduction arbitrary: r rule: language_coinduct_upto_regular)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. \<oo> (Times (Star r) (Star r)) = \<oo> (Star r) \<and> (\<forall>x. regular_cong (\<lambda>L__ K__. \<exists>r. L__ = Times (Star r) (Star r) \<and> K__ = Star r) (\<dd> (Times (Star r) (Star r)) x) (\<dd> (Star r) x))
[PROOF STEP]
case Lang
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>r. \<oo> (Times (Star r) (Star r)) = \<oo> (Star r) \<and> (\<forall>x. regular_cong (\<lambda>L__ K__. \<exists>r. L__ = Times (Star r) (Star r) \<and> K__ = Star r) (\<dd> (Times (Star r) (Star r)) x) (\<dd> (Star r) x))
[PROOF STEP]
have *: "\<And>r s. Plus (Times r s) r = Times r (Plus s One)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r s. Plus (Times r s) r = Times r (Plus s One)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Plus (Times ?r ?s) ?r = Times ?r (Plus ?s One)

goal (1 subgoal):
 1. \<And>r. \<oo> (Times (Star r) (Star r)) = \<oo> (Star r) \<and> (\<forall>x. regular_cong (\<lambda>L__ K__. \<exists>r. L__ = Times (Star r) (Star r) \<and> K__ = Star r) (\<dd> (Times (Star r) (Star r)) x) (\<dd> (Star r) x))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> (Times (Star r) (Star r)) = \<oo> (Star r) \<and> (\<forall>x. regular_cong (\<lambda>L__ K__. \<exists>r. L__ = Times (Star r) (Star r) \<and> K__ = Star r) (\<dd> (Times (Star r) (Star r)) x) (\<dd> (Star r) x))
[PROOF STEP]
by (auto simp del: Times_PlusR Plus_ACI simp: Times_PlusR[symmetric] *)
[PROOF STATE]
proof (state)
this:
\<oo> (Times (Star r) (Star r)) = \<oo> (Star r) \<and> (\<forall>x. regular_cong (\<lambda>L__ K__. \<exists>r. L__ = Times (Star r) (Star r) \<and> K__ = Star r) (\<dd> (Times (Star r) (Star r)) x) (\<dd> (Star r) x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Zero_One[simp]: "Zero \<noteq> One"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Zero \<noteq> One
[PROOF STEP]
by (metis One.simps(1) Zero.simps(1))


[STATEMENT]
lemma \<oo>_mono[dest]: "r \<le> s \<Longrightarrow> \<oo> r \<Longrightarrow> \<oo> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<le> s; \<oo> r\<rbrakk> \<Longrightarrow> \<oo> s
[PROOF STEP]
unfolding less_eq_language_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Plus r s = s; \<oo> r\<rbrakk> \<Longrightarrow> \<oo> s
[PROOF STEP]
by (auto dest: arg_cong[of _ _ \<oo>])


[STATEMENT]
lemma \<dd>_mono[dest]: "r \<le> s \<Longrightarrow> \<dd> r a \<le> \<dd> s a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<le> s \<Longrightarrow> \<dd> r a \<le> \<dd> s a
[PROOF STEP]
unfolding less_eq_language_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus r s = s \<Longrightarrow> Plus (\<dd> r a) (\<dd> s a) = \<dd> s a
[PROOF STEP]
by (metis Plus.simps(2))


[STATEMENT]
theorem language_simulation_coinduction[consumes 1, case_names Lang, coinduct pred]:
  assumes "R L K"
      and "(\<And>L K. R L K \<Longrightarrow> \<oo> L \<le> \<oo> K \<and> (\<forall>x. R (\<dd> L x) (\<dd> K x)))"
  shows "L \<le> K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L \<le> K
[PROOF STEP]
using \<open>R L K\<close>
[PROOF STATE]
proof (prove)
using this:
R L K

goal (1 subgoal):
 1. L \<le> K
[PROOF STEP]
unfolding less_eq_language_def
[PROOF STATE]
proof (prove)
using this:
R L K

goal (1 subgoal):
 1. Plus L K = K
[PROOF STEP]
by (coinduction arbitrary: L K) (auto dest!: assms(2))


[STATEMENT]
lemma le_PlusL[intro!, simp]: "r \<le> Plus r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<le> Plus r s
[PROOF STEP]
by (coinduction arbitrary: r s) auto


[STATEMENT]
lemma le_PlusR[intro!, simp]: "s \<le> Plus r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<le> Plus r s
[PROOF STEP]
by (coinduction arbitrary: r s) auto


[STATEMENT]
theorem language_simulation_coinduction_upto_Plus_Times[consumes 1, case_names Lang, coinduct pred]:
  assumes R: "R L K"
      and hyp: "(\<And>L K. R L K \<Longrightarrow> \<oo> L \<le> \<oo> K \<and> (\<forall>x. Plus_Times_pre_cong R (\<dd> L x) (\<dd> K x)))"
    shows "L \<le> K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L \<le> K
[PROOF STEP]
proof (coinduct rule: language_simulation_coinduction[of "Plus_Times_pre_cong R"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Plus_Times_pre_cong R L K
 2. \<And>L K. Plus_Times_pre_cong R L K \<Longrightarrow> \<oo> L \<le> \<oo> K \<and> (\<forall>x. Plus_Times_pre_cong R (\<dd> L x) (\<dd> K x))
[PROOF STEP]
fix L K
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Plus_Times_pre_cong R L K
 2. \<And>L K. Plus_Times_pre_cong R L K \<Longrightarrow> \<oo> L \<le> \<oo> K \<and> (\<forall>x. Plus_Times_pre_cong R (\<dd> L x) (\<dd> K x))
[PROOF STEP]
assume "Plus_Times_pre_cong R L K"
[PROOF STATE]
proof (state)
this:
Plus_Times_pre_cong R L K

goal (2 subgoals):
 1. Plus_Times_pre_cong R L K
 2. \<And>L K. Plus_Times_pre_cong R L K \<Longrightarrow> \<oo> L \<le> \<oo> K \<and> (\<forall>x. Plus_Times_pre_cong R (\<dd> L x) (\<dd> K x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plus_Times_pre_cong R L K
[PROOF STEP]
show "\<oo> L \<le> \<oo> K \<and> (\<forall>x. Plus_Times_pre_cong R (\<dd> L x) (\<dd> K x))"
[PROOF STATE]
proof (prove)
using this:
Plus_Times_pre_cong R L K

goal (1 subgoal):
 1. \<oo> L \<le> \<oo> K \<and> (\<forall>x. Plus_Times_pre_cong R (\<dd> L x) (\<dd> K x))
[PROOF STEP]
by (induct rule: Plus_Times_pre_cong.induct) (auto dest: hyp)
[PROOF STATE]
proof (state)
this:
\<oo> L \<le> \<oo> K \<and> (\<forall>x. Plus_Times_pre_cong R (\<dd> L x) (\<dd> K x))

goal (1 subgoal):
 1. Plus_Times_pre_cong R L K
[PROOF STEP]
qed (intro pre_Base R)


[STATEMENT]
lemma ge_One[simp]: "One \<le> r \<longleftrightarrow> \<oo> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (One \<le> r) = \<oo> r
[PROOF STEP]
unfolding less_eq_language_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Plus One r = r) = \<oo> r
[PROOF STEP]
by (metis One.sel(1) Plus.sel(1) Plus_OneL)


[STATEMENT]
lemma Plus_mono: "\<lbrakk>r1 \<le> s1; r2 \<le> s2\<rbrakk> \<Longrightarrow> Plus r1 r2 \<le> Plus s1 s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r1 \<le> s1; r2 \<le> s2\<rbrakk> \<Longrightarrow> Plus r1 r2 \<le> Plus s1 s2
[PROOF STEP]
by (coinduction arbitrary: r1 r2 s1 s2) (auto elim!: \<dd>_mono)


[STATEMENT]
lemma Plus_upper: "\<lbrakk>r1 \<le> s; r2 \<le> s\<rbrakk> \<Longrightarrow> Plus r1 r2 \<le> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r1 \<le> s; r2 \<le> s\<rbrakk> \<Longrightarrow> Plus r1 r2 \<le> s
[PROOF STEP]
by (coinduction arbitrary: r1 r2 s) auto


[STATEMENT]
lemma Inter_mono: "\<lbrakk>r1 \<le> s1; r2 \<le> s2\<rbrakk> \<Longrightarrow> Inter r1 r2 \<le> Inter s1 s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r1 \<le> s1; r2 \<le> s2\<rbrakk> \<Longrightarrow> Inter r1 r2 \<le> Inter s1 s2
[PROOF STEP]
by (coinduction arbitrary: r1 r2 s1 s2) (force elim!: \<dd>_mono)


[STATEMENT]
lemma Times_mono: "\<lbrakk>r1 \<le> s1; r2 \<le> s2\<rbrakk> \<Longrightarrow> Times r1 r2 \<le> Times s1 s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r1 \<le> s1; r2 \<le> s2\<rbrakk> \<Longrightarrow> Times r1 r2 \<le> Times s1 s2
[PROOF STEP]
by (coinduction arbitrary: r1 r2 s1 s2) (auto 0 3 elim!: \<dd>_mono)


[STATEMENT]
theorem le_StarL: "Plus One (Times r (Star r)) \<le> Star r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus One (Times r (Star r)) \<le> Star r
[PROOF STEP]
by coinduction auto


[STATEMENT]
theorem le_StarR: "Plus One (Times (Star r) r) \<le> Star r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus One (Times (Star r) r) \<le> Star r
[PROOF STEP]
by (rule order_eq_refl[OF Star_unfoldR[symmetric]])


[STATEMENT]
lemma le_TimesL[intro, simp]: "\<oo> s \<Longrightarrow> r \<le> Times r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> s \<Longrightarrow> r \<le> Times r s
[PROOF STEP]
by (coinduction arbitrary: r) auto


[STATEMENT]
lemma le_TimesR[intro, simp]: "\<oo> r \<Longrightarrow> s \<le> Times r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> r \<Longrightarrow> s \<le> Times r s
[PROOF STEP]
by coinduction auto


[STATEMENT]
lemma Plus_le_iff: "Plus r s \<le> t \<longleftrightarrow> r \<le> t \<and> s \<le> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Plus r s \<le> t) = (r \<le> t \<and> s \<le> t)
[PROOF STEP]
unfolding less_eq_language_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Plus (Plus r s) t = t) = (Plus r t = t \<and> Plus s t = t)
[PROOF STEP]
by (metis Plus_assoc Plus_idem_assoc Plus_rotate)


[STATEMENT]
lemma Plus_Times_pre_cong_mono:
  "L' \<le> L \<Longrightarrow> K \<le> K' \<Longrightarrow> Plus_Times_pre_cong R L K \<Longrightarrow> Plus_Times_pre_cong R L' K'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>L' \<le> L; K \<le> K'; Plus_Times_pre_cong R L K\<rbrakk> \<Longrightarrow> Plus_Times_pre_cong R L' K'
[PROOF STEP]
by (metis pre_Trans pre_Less)


[STATEMENT]
theorem ardenL: "Plus r (Times s x) \<le> x \<Longrightarrow> Times (Star s) r \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus r (Times s x) \<le> x \<Longrightarrow> Times (Star s) r \<le> x
[PROOF STEP]
proof (coinduction arbitrary: r s x)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r s x. Plus r (Times s x) \<le> x \<Longrightarrow> \<oo> (Times (Star s) r) \<le> \<oo> x \<and> (\<forall>xa. Plus_Times_pre_cong (\<lambda>L__ K__. \<exists>r s x. L__ = Times (Star s) r \<and> K__ = x \<and> Plus r (Times s x) \<le> x) (\<dd> (Times (Star s) r) xa) (\<dd> x xa))
[PROOF STEP]
case Lang
[PROOF STATE]
proof (state)
this:
Plus r (Times s x) \<le> x

goal (1 subgoal):
 1. \<And>r s x. Plus r (Times s x) \<le> x \<Longrightarrow> \<oo> (Times (Star s) r) \<le> \<oo> x \<and> (\<forall>xa. Plus_Times_pre_cong (\<lambda>L__ K__. \<exists>r s x. L__ = Times (Star s) r \<and> K__ = x \<and> Plus r (Times s x) \<le> x) (\<dd> (Times (Star s) r) xa) (\<dd> x xa))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plus r (Times s x) \<le> x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Plus r (Times s x) \<le> x

goal (1 subgoal):
 1. \<oo> (Times (Star s) r) \<le> \<oo> x \<and> (\<forall>x. Plus_Times_pre_cong (\<lambda>L__ K__. \<exists>r s x. L__ = Times (Star s) r \<and> K__ = x \<and> Plus r (Times s x) \<le> x) (\<dd> (Times (Star s) r) x) (\<dd> x x))
[PROOF STEP]
by (subst Plus_Times_pre_cong_mono[OF order_refl \<dd>_mono[OF Lang]]) auto
[PROOF STATE]
proof (state)
this:
\<oo> (Times (Star s) r) \<le> \<oo> x \<and> (\<forall>x. Plus_Times_pre_cong (\<lambda>L__ K__. \<exists>r s x. L__ = Times (Star s) r \<and> K__ = x \<and> Plus r (Times s x) \<le> x) (\<dd> (Times (Star s) r) x) (\<dd> x x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ardenR: "Plus r (Times x s) \<le> x \<Longrightarrow> Times r (Star s) \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus r (Times x s) \<le> x \<Longrightarrow> Times r (Star s) \<le> x
[PROOF STEP]
proof (coinduction arbitrary: r s x)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r s x. Plus r (Times x s) \<le> x \<Longrightarrow> \<oo> (Times r (Star s)) \<le> \<oo> x \<and> (\<forall>xa. Plus_Times_pre_cong (\<lambda>L__ K__. \<exists>r s x. L__ = Times r (Star s) \<and> K__ = x \<and> Plus r (Times x s) \<le> x) (\<dd> (Times r (Star s)) xa) (\<dd> x xa))
[PROOF STEP]
case Lang
[PROOF STATE]
proof (state)
this:
Plus r (Times x s) \<le> x

goal (1 subgoal):
 1. \<And>r s x. Plus r (Times x s) \<le> x \<Longrightarrow> \<oo> (Times r (Star s)) \<le> \<oo> x \<and> (\<forall>xa. Plus_Times_pre_cong (\<lambda>L__ K__. \<exists>r s x. L__ = Times r (Star s) \<and> K__ = x \<and> Plus r (Times x s) \<le> x) (\<dd> (Times r (Star s)) xa) (\<dd> x xa))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plus r (Times x s) \<le> x
[PROOF STEP]
have "Plus_Times_pre_cong (\<lambda>L K. \<exists>r s. L = Times r (Star s) \<and> Plus r (Times K s) \<le> K)
    (\<dd> (Times r (Star s)) a) (\<dd> x a)" for a
[PROOF STATE]
proof (prove)
using this:
Plus r (Times x s) \<le> x

goal (1 subgoal):
 1. Plus_Times_pre_cong (\<lambda>L K. \<exists>r s. L = Times r (Star s) \<and> Plus r (Times K s) \<le> K) (\<dd> (Times r (Star s)) a) (\<dd> x a)
[PROOF STEP]
using \<dd>_mono[OF Lang, of a]
[PROOF STATE]
proof (prove)
using this:
Plus r (Times x s) \<le> x
\<dd> (Plus r (Times x s)) a \<le> \<dd> x a

goal (1 subgoal):
 1. Plus_Times_pre_cong (\<lambda>L K. \<exists>r s. L = Times r (Star s) \<and> Plus r (Times K s) \<le> K) (\<dd> (Times r (Star s)) a) (\<dd> x a)
[PROOF STEP]
by (auto 0 4 simp del: Times_PlusL simp: Times_PlusL[symmetric] Plus_le_iff split: if_splits)
[PROOF STATE]
proof (state)
this:
Plus_Times_pre_cong (\<lambda>L K. \<exists>r s. L = Times r (Star s) \<and> Plus r (Times K s) \<le> K) (\<dd> (Times r (Star s)) ?a) (\<dd> x ?a)

goal (1 subgoal):
 1. \<And>r s x. Plus r (Times x s) \<le> x \<Longrightarrow> \<oo> (Times r (Star s)) \<le> \<oo> x \<and> (\<forall>xa. Plus_Times_pre_cong (\<lambda>L__ K__. \<exists>r s x. L__ = Times r (Star s) \<and> K__ = x \<and> Plus r (Times x s) \<le> x) (\<dd> (Times r (Star s)) xa) (\<dd> x xa))
[PROOF STEP]
with Lang
[PROOF STATE]
proof (chain)
picking this:
Plus r (Times x s) \<le> x
Plus_Times_pre_cong (\<lambda>L K. \<exists>r s. L = Times r (Star s) \<and> Plus r (Times K s) \<le> K) (\<dd> (Times r (Star s)) ?a) (\<dd> x ?a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Plus r (Times x s) \<le> x
Plus_Times_pre_cong (\<lambda>L K. \<exists>r s. L = Times r (Star s) \<and> Plus r (Times K s) \<le> K) (\<dd> (Times r (Star s)) ?a) (\<dd> x ?a)

goal (1 subgoal):
 1. \<oo> (Times r (Star s)) \<le> \<oo> x \<and> (\<forall>x. Plus_Times_pre_cong (\<lambda>L__ K__. \<exists>r s x. L__ = Times r (Star s) \<and> K__ = x \<and> Plus r (Times x s) \<le> x) (\<dd> (Times r (Star s)) x) (\<dd> x x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<oo> (Times r (Star s)) \<le> \<oo> x \<and> (\<forall>x. Plus_Times_pre_cong (\<lambda>L__ K__. \<exists>r s x. L__ = Times r (Star s) \<and> K__ = x \<and> Plus r (Times x s) \<le> x) (\<dd> (Times r (Star s)) x) (\<dd> x x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma le_Star[intro!, simp]: "s \<le> Star s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<le> Star s
[PROOF STEP]
by coinduction auto


[STATEMENT]
lemma Star_mono: "r \<le> s \<Longrightarrow> Star r \<le> Star s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<le> s \<Longrightarrow> Star r \<le> Star s
[PROOF STEP]
by coinduction auto


[STATEMENT]
lemma Not_antimono: "r \<le> s \<Longrightarrow> Not s \<le> Not r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<le> s \<Longrightarrow> Coinductive_Language.Not s \<le> Coinductive_Language.Not r
[PROOF STEP]
by (coinduction arbitrary: r s) auto


[STATEMENT]
lemma Not_Plus[simp]: "Not (Plus r s) = Inter (Not r) (Not s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Coinductive_Language.Not (Plus r s) = Inter (Coinductive_Language.Not r) (Coinductive_Language.Not s)
[PROOF STEP]
by (coinduction arbitrary: r s) auto


[STATEMENT]
lemma Not_Inter[simp]: "Not (Inter r s) = Plus (Not r) (Not s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Coinductive_Language.Not (Inter r s) = Plus (Coinductive_Language.Not r) (Coinductive_Language.Not s)
[PROOF STEP]
by (coinduction arbitrary: r s) auto


[STATEMENT]
lemma Inter_assoc[simp]: "Inter (Inter r s) t = Inter r (Inter s t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inter (Inter r s) t = Inter r (Inter s t)
[PROOF STEP]
by (coinduction arbitrary: r s t) auto


[STATEMENT]
lemma Inter_comm: "Inter r s = Inter s r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inter r s = Inter s r
[PROOF STEP]
by (coinduction arbitrary: r s) auto


[STATEMENT]
lemma Inter_idem[simp]: "Inter r r = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inter r r = r
[PROOF STEP]
by (coinduction arbitrary: r) auto


[STATEMENT]
lemma Inter_ZeroL[simp]: "Inter Zero r = Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inter Zero r = Zero
[PROOF STEP]
by (coinduction arbitrary: r) auto


[STATEMENT]
lemma Inter_ZeroR[simp]: "Inter r Zero = Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inter r Zero = Zero
[PROOF STEP]
by (coinduction arbitrary: r) auto


[STATEMENT]
lemma Inter_FullL[simp]: "Inter Full r = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inter \<Sigma>\<^sup>* r = r
[PROOF STEP]
by (coinduction arbitrary: r) auto


[STATEMENT]
lemma Inter_FullR[simp]: "Inter r Full = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inter r \<Sigma>\<^sup>* = r
[PROOF STEP]
by (coinduction arbitrary: r) auto


[STATEMENT]
lemma Plus_FullL[simp]: "Plus Full r = Full"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus \<Sigma>\<^sup>* r = \<Sigma>\<^sup>*
[PROOF STEP]
by (coinduction arbitrary: r) auto


[STATEMENT]
lemma Plus_FullR[simp]: "Plus r Full = Full"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus r \<Sigma>\<^sup>* = \<Sigma>\<^sup>*
[PROOF STEP]
by (coinduction arbitrary: r) auto


[STATEMENT]
lemma Not_Not[simp]: "Not (Not r) = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Coinductive_Language.Not (Coinductive_Language.Not r) = r
[PROOF STEP]
by (coinduction arbitrary: r) auto


[STATEMENT]
lemma Not_Zero[simp]: "Not Zero = Full"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Coinductive_Language.Not Zero = \<Sigma>\<^sup>*
[PROOF STEP]
by coinduction simp


[STATEMENT]
lemma Not_Full[simp]: "Not Full = Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Coinductive_Language.Not \<Sigma>\<^sup>* = Zero
[PROOF STEP]
by coinduction simp


[STATEMENT]
lemma bisimulation:
  assumes "Times r s = Times s t"
  shows "Times (Star r) s = Times s (Star t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times (Star r) s = Times s (Star t)
[PROOF STEP]
proof (rule antisym[OF ardenL[OF Plus_upper[OF le_TimesL]] ardenR[OF Plus_upper[OF le_TimesR]]])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<oo> (Star t)
 2. Times r (Times s (Star t)) \<le> Times s (Star t)
 3. \<oo> (Star r)
 4. Times (Times (Star r) s) t \<le> Times (Star r) s
[PROOF STEP]
show "Times r (Times s (Star t)) \<le> Times s (Star t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times r (Times s (Star t)) \<le> Times s (Star t)
[PROOF STEP]
by (rule order_trans[OF _
        Times_mono[OF order_refl ord_le_eq_trans[OF le_PlusR Star_unfoldL[symmetric]]]])
      (simp only: assms Times_assoc[symmetric])
[PROOF STATE]
proof (state)
this:
Times r (Times s (Star t)) \<le> Times s (Star t)

goal (3 subgoals):
 1. \<oo> (Star t)
 2. \<oo> (Star r)
 3. Times (Times (Star r) s) t \<le> Times (Star r) s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<oo> (Star t)
 2. \<oo> (Star r)
 3. Times (Times (Star r) s) t \<le> Times (Star r) s
[PROOF STEP]
show "Times (Times (Star r) s) t \<le> Times (Star r) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times (Times (Star r) s) t \<le> Times (Star r) s
[PROOF STEP]
by (rule order_trans[OF _
        Times_mono[OF ord_le_eq_trans[OF le_PlusR Star_unfoldR[symmetric]] order_refl]])
      (simp only: assms Times_assoc)
[PROOF STATE]
proof (state)
this:
Times (Times (Star r) s) t \<le> Times (Star r) s

goal (2 subgoals):
 1. \<oo> (Star t)
 2. \<oo> (Star r)
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma sliding: "Times (Star (Times r s)) r = Times r (Star (Times s r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times (Star (Times r s)) r = Times r (Star (Times s r))
[PROOF STEP]
proof (rule antisym[OF ardenL[OF Plus_upper[OF le_TimesL]] ardenR[OF Plus_upper[OF le_TimesR]]])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<oo> (Star (Times s r))
 2. Times (Times r s) (Times r (Star (Times s r))) \<le> Times r (Star (Times s r))
 3. \<oo> (Star (Times r s))
 4. Times (Times (Star (Times r s)) r) (Times s r) \<le> Times (Star (Times r s)) r
[PROOF STEP]
show "Times (Times r s) (Times r (Star (Times s r))) \<le> Times r (Star (Times s r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times (Times r s) (Times r (Star (Times s r))) \<le> Times r (Star (Times s r))
[PROOF STEP]
by (rule order_trans[OF _
        Times_mono[OF order_refl ord_le_eq_trans[OF le_PlusR Star_unfoldL[symmetric]]]]) simp
[PROOF STATE]
proof (state)
this:
Times (Times r s) (Times r (Star (Times s r))) \<le> Times r (Star (Times s r))

goal (3 subgoals):
 1. \<oo> (Star (Times s r))
 2. \<oo> (Star (Times r s))
 3. Times (Times (Star (Times r s)) r) (Times s r) \<le> Times (Star (Times r s)) r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<oo> (Star (Times s r))
 2. \<oo> (Star (Times r s))
 3. Times (Times (Star (Times r s)) r) (Times s r) \<le> Times (Star (Times r s)) r
[PROOF STEP]
show "Times (Times (Star (Times r s)) r) (Times s r) \<le> Times (Star (Times r s)) r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times (Times (Star (Times r s)) r) (Times s r) \<le> Times (Star (Times r s)) r
[PROOF STEP]
by (rule order_trans[OF _
        Times_mono[OF ord_le_eq_trans[OF le_PlusR Star_unfoldR[symmetric]] order_refl]]) simp
[PROOF STATE]
proof (state)
this:
Times (Times (Star (Times r s)) r) (Times s r) \<le> Times (Star (Times r s)) r

goal (2 subgoals):
 1. \<oo> (Star (Times s r))
 2. \<oo> (Star (Times r s))
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma denesting: "Star (Plus r s) = Times (Star r) (Star (Times s (Star r)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Star (Plus r s) = Times (Star r) (Star (Times s (Star r)))
[PROOF STEP]
proof (rule antisym[OF ord_eq_le_trans[OF Times_OneR[symmetric] ardenL[OF Plus_upper]]
   ardenR[OF Plus_upper[OF Star_mono[OF le_PlusL]]]])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. One \<le> Times (Star r) (Star (Times s (Star r)))
 2. Times (Plus r s) (Times (Star r) (Star (Times s (Star r)))) \<le> Times (Star r) (Star (Times s (Star r)))
 3. Times (Star (Plus r s)) (Times s (Star r)) \<le> Star (Plus r s)
[PROOF STEP]
show "Times (Plus r s) (Times (Star r) (Star (Times s (Star r))))
    \<le> Times (Star r) (Star (Times s (Star r)))" (is "Times _ ?L \<le> ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times (Plus r s) (Times (Star r) (Star (Times s (Star r)))) \<le> Times (Star r) (Star (Times s (Star r)))
[PROOF STEP]
unfolding Times_PlusL
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus (Times r (Times (Star r) (Star (Times s (Star r))))) (Times s (Times (Star r) (Star (Times s (Star r))))) \<le> Times (Star r) (Star (Times s (Star r)))
[PROOF STEP]
by (rule Plus_upper,
      metis Star_unfoldL Times_assoc Times_mono le_PlusR order_refl,
      metis Star_unfoldL Times_assoc \<oo>_Star le_PlusR le_TimesR order_trans)
[PROOF STATE]
proof (state)
this:
Times (Plus r s) (Times (Star r) (Star (Times s (Star r)))) \<le> Times (Star r) (Star (Times s (Star r)))

goal (2 subgoals):
 1. One \<le> Times (Star r) (Star (Times s (Star r)))
 2. Times (Star (Plus r s)) (Times s (Star r)) \<le> Star (Plus r s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. One \<le> Times (Star r) (Star (Times s (Star r)))
 2. Times (Star (Plus r s)) (Times s (Star r)) \<le> Star (Plus r s)
[PROOF STEP]
show "Times (Star (Plus r s)) (Times s (Star r)) \<le> Star (Plus r s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times (Star (Plus r s)) (Times s (Star r)) \<le> Star (Plus r s)
[PROOF STEP]
by (metis Plus_comm Star_unfoldL Times_PlusR Times_assoc ardenR bisimulation le_PlusR)
[PROOF STATE]
proof (state)
this:
Times (Star (Plus r s)) (Times s (Star r)) \<le> Star (Plus r s)

goal (1 subgoal):
 1. One \<le> Times (Star r) (Star (Times s (Star r)))
[PROOF STEP]
qed simp


[STATEMENT]
lemma \<oo>_foldr_Plus: "\<oo> (foldr Plus xs s) = (\<exists>x\<in>set (s # xs). \<oo> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> (foldr Plus xs s) = (\<exists>x\<in>set (s # xs). \<oo> x)
[PROOF STEP]
by (induct xs arbitrary: s) auto


[STATEMENT]
lemma \<dd>_foldr_Plus: "\<dd> (foldr Plus xs s) a = foldr Plus (map (\<lambda>r. \<dd> r a) xs) (\<dd> s a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dd> (foldr Plus xs s) a = foldr Plus (map (\<lambda>r. \<dd> r a) xs) (\<dd> s a)
[PROOF STEP]
by (induct xs arbitrary: s) simp_all


[STATEMENT]
lemma \<dd>_PLUS[simp]: "\<dd> (PLUS xs) a = PLUS (map (\<lambda>r. \<dd> r a) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dd> (PLUS xs) a = PLUS (map (\<lambda>r. \<dd> r a) xs)
[PROOF STEP]
unfolding PLUS_def \<dd>_foldr_Plus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldr Plus (map (\<lambda>r. \<dd> r a) xs) (\<dd> Zero a) = foldr Plus (map (\<lambda>r. \<dd> r a) xs) Zero
[PROOF STEP]
by simp


[STATEMENT]
lemma \<oo>_foldr_Times: "\<oo> (foldr Times xs s) = (\<forall>x\<in>set (s # xs). \<oo> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> (foldr Times xs s) = (\<forall>x\<in>set (s # xs). \<oo> x)
[PROOF STEP]
by (induct xs) (auto simp: PLUS_def)


[STATEMENT]
lemma tails_snoc[simp]: "tails (xs @ [x]) = map (\<lambda>ys. ys @ [x]) (tails xs) @ [[]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tails (xs @ [x]) = map (\<lambda>ys. ys @ [x]) (tails xs) @ [[]]
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma length_tails[simp]: "length (tails xs) = Suc (length xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (tails xs) = Suc (length xs)
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma \<dd>_foldr_Times: "\<dd> (foldr Times xs s) a =
  (let n = length (takeWhile \<oo> xs)
  in PLUS (map (\<lambda>zs. TIMES (\<dd> (hd zs) a # tl zs)) (take (Suc n) (tails (xs @ [s])))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dd> (foldr Times xs s) a = (let n = length (takeWhile \<oo> xs) in PLUS (map (\<lambda>zs. TIMES (\<dd> (hd zs) a # tl zs)) (take (Suc n) (tails (xs @ [s])))))
[PROOF STEP]
by (induct xs) (auto simp: TIMES_def PLUS_def Let_def foldr_map o_def)


[STATEMENT]
lemma \<oo>_TIMES[simp]: "\<oo> (TIMES xs) = (\<forall>x\<in>set xs. \<oo> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> (TIMES xs) = (\<forall>x\<in>set xs. \<oo> x)
[PROOF STEP]
unfolding TIMES_def \<oo>_foldr_Times
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ball (set (One # xs)) \<oo> = (\<forall>x\<in>set xs. \<oo> x)
[PROOF STEP]
by simp


[STATEMENT]
lemma TIMES_snoc_One[simp]: "TIMES (xs @ [One]) = TIMES xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TIMES (xs @ [One]) = TIMES xs
[PROOF STEP]
by (induct xs) (auto simp: TIMES_def)


[STATEMENT]
lemma \<dd>_TIMES[simp]: "\<dd> (TIMES xs) a = (let n = length (takeWhile \<oo> xs)
  in PLUS (map (\<lambda>zs. TIMES (\<dd> (hd zs) a # tl zs)) (take (Suc n) (tails (xs @ [One])))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dd> (TIMES xs) a = (let n = length (takeWhile \<oo> xs) in PLUS (map (\<lambda>zs. TIMES (\<dd> (hd zs) a # tl zs)) (take (Suc n) (tails (xs @ [One])))))
[PROOF STEP]
unfolding TIMES_def \<dd>_foldr_Times
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let n = length (takeWhile \<oo> xs) in PLUS (map (\<lambda>zs. foldr Times (\<dd> (hd zs) a # tl zs) One) (take (Suc n) (tails (xs @ [One]))))) = (let n = length (takeWhile \<oo> xs) in PLUS (map (\<lambda>zs. foldr Times (\<dd> (hd zs) a # tl zs) One) (take (Suc n) (tails (xs @ [One])))))
[PROOF STEP]
by simp


[STATEMENT]
lemma in_language_to_language[simp]: "Collect (in_language (to_language L)) = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Collect (in_language (to_language L)) = L
[PROOF STEP]
proof (rule set_eqI, unfold mem_Collect_eq)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. in_language (to_language L) x = (x \<in> L)
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. in_language (to_language L) x = (x \<in> L)
[PROOF STEP]
show "in_language (to_language L) w = (w \<in> L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_language (to_language L) w = (w \<in> L)
[PROOF STEP]
by (induct w arbitrary: L) auto
[PROOF STATE]
proof (state)
this:
in_language (to_language L) w = (w \<in> L)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma to_language_in_language[simp]: "to_language (Collect (in_language L)) = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_language (Collect (in_language L)) = L
[PROOF STEP]
by (coinduction arbitrary: L) auto


[STATEMENT]
lemma in_language_bij: "bij (Collect o in_language)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij (Collect \<circ> in_language)
[PROOF STEP]
proof (rule bijI', unfold o_apply, safe)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. Collect (in_language x) = Collect (in_language y) \<Longrightarrow> x = y
 2. \<And>y. \<exists>x. y = Collect (in_language x)
[PROOF STEP]
fix L R :: "'a language"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. Collect (in_language x) = Collect (in_language y) \<Longrightarrow> x = y
 2. \<And>y. \<exists>x. y = Collect (in_language x)
[PROOF STEP]
assume "Collect (in_language L) = Collect (in_language R)"
[PROOF STATE]
proof (state)
this:
Collect (in_language L) = Collect (in_language R)

goal (2 subgoals):
 1. \<And>x y. Collect (in_language x) = Collect (in_language y) \<Longrightarrow> x = y
 2. \<And>y. \<exists>x. y = Collect (in_language x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Collect (in_language L) = Collect (in_language R)
[PROOF STEP]
show "L = R"
[PROOF STATE]
proof (prove)
using this:
Collect (in_language L) = Collect (in_language R)

goal (1 subgoal):
 1. L = R
[PROOF STEP]
unfolding set_eq_iff mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
\<forall>x. in_language L x = in_language R x

goal (1 subgoal):
 1. L = R
[PROOF STEP]
by (coinduction arbitrary: L R) (metis in_language.simps)
[PROOF STATE]
proof (state)
this:
L = R

goal (1 subgoal):
 1. \<And>y. \<exists>x. y = Collect (in_language x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>x. y = Collect (in_language x)
[PROOF STEP]
fix L :: "'a list set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>x. y = Collect (in_language x)
[PROOF STEP]
have "L = Collect (in_language (to_language L))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L = Collect (in_language (to_language L))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
L = Collect (in_language (to_language L))

goal (1 subgoal):
 1. \<And>y. \<exists>x. y = Collect (in_language x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Collect (in_language (to_language L))
[PROOF STEP]
show "\<exists>K. L = Collect (in_language K)"
[PROOF STATE]
proof (prove)
using this:
L = Collect (in_language (to_language L))

goal (1 subgoal):
 1. \<exists>K. L = Collect (in_language K)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>K. L = Collect (in_language K)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma to_language_bij: "bij to_language"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij to_language
[PROOF STEP]
by (rule o_bij[of "Collect o in_language"]) (simp_all add: fun_eq_iff)


[STATEMENT]
lemma precedes_mem:
  assumes "x \<preceq> y in xs"
  shows "x \<in> set xs" "y \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs &&& y \<in> set xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in xs

goal (1 subgoal):
 1. x \<in> set xs &&& y \<in> set xs
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l r. xs = l @ x # r \<and> y \<in> set (x # r)

goal (1 subgoal):
 1. x \<in> set xs &&& y \<in> set xs
[PROOF STEP]
by auto


[STATEMENT]
lemma head_precedes:
  assumes "y \<in> set (x # xs)"
  shows "x \<preceq> y in (x # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<preceq> y in (x # xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
y \<in> set (x # xs)

goal (1 subgoal):
 1. x \<preceq> y in (x # xs)
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
y \<in> set (x # xs)

goal (1 subgoal):
 1. \<exists>l r. x # xs = l @ x # r \<and> y \<in> set (x # r)
[PROOF STEP]
by force


[STATEMENT]
lemma precedes_in_tail:
  assumes "x \<noteq> z"
  shows "x \<preceq> y in (z # zs) \<longleftrightarrow> x \<preceq> y in zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<preceq> y in (z # zs)) = (x \<preceq> y in zs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> z

goal (1 subgoal):
 1. (x \<preceq> y in (z # zs)) = (x \<preceq> y in zs)
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
x \<noteq> z

goal (1 subgoal):
 1. (\<exists>l r. z # zs = l @ x # r \<and> y \<in> set (x # r)) = (\<exists>l r. zs = l @ x # r \<and> y \<in> set (x # r))
[PROOF STEP]
by (auto simp: Cons_eq_append_conv)


[STATEMENT]
lemma tail_not_precedes:
  assumes "y \<preceq> x in (x # xs)" "x \<notin> set xs"
  shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
y \<preceq> x in (x # xs)
x \<notin> set xs

goal (1 subgoal):
 1. x = y
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l r. x # xs = l @ y # r \<and> x \<in> set (y # r)
x \<notin> set xs

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (metis Cons_eq_append_conv Un_iff list.inject set_append)


[STATEMENT]
lemma split_list_precedes:
  assumes "y \<in> set (ys @ [x])"
  shows "y \<preceq> x in (ys @ x # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<preceq> x in (ys @ x # xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
y \<in> set (ys @ [x])

goal (1 subgoal):
 1. y \<preceq> x in (ys @ x # xs)
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
y \<in> set (ys @ [x])

goal (1 subgoal):
 1. \<exists>l r. ys @ x # xs = l @ y # r \<and> x \<in> set (y # r)
[PROOF STEP]
by (metis append_Cons append_assoc in_set_conv_decomp
            rotate1.simps(2) set_ConsD set_rotate1)


[STATEMENT]
lemma precedes_refl [simp]: "(x \<preceq> x in xs) = (x \<in> set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<preceq> x in xs) = (x \<in> set xs)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<preceq> x in xs \<Longrightarrow> x \<in> set xs
 2. x \<in> set xs \<Longrightarrow> x \<preceq> x in xs
[PROOF STEP]
assume "x \<preceq> x in xs"
[PROOF STATE]
proof (state)
this:
x \<preceq> x in xs

goal (2 subgoals):
 1. x \<preceq> x in xs \<Longrightarrow> x \<in> set xs
 2. x \<in> set xs \<Longrightarrow> x \<preceq> x in xs
[PROOF STEP]
thus "x \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
x \<preceq> x in xs

goal (1 subgoal):
 1. x \<in> set xs
[PROOF STEP]
by (simp add: precedes_mem)
[PROOF STATE]
proof (state)
this:
x \<in> set xs

goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> x \<preceq> x in xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> x \<preceq> x in xs
[PROOF STEP]
assume "x \<in> set xs"
[PROOF STATE]
proof (state)
this:
x \<in> set xs

goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> x \<preceq> x in xs
[PROOF STEP]
from this[THEN split_list]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ys zs. xs = ys @ x # zs
[PROOF STEP]
show "x \<preceq> x in xs"
[PROOF STATE]
proof (prove)
using this:
\<exists>ys zs. xs = ys @ x # zs

goal (1 subgoal):
 1. x \<preceq> x in xs
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
\<exists>ys zs. xs = ys @ x # zs

goal (1 subgoal):
 1. \<exists>l r. xs = l @ x # r \<and> x \<in> set (x # r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<preceq> x in xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma precedes_append_left:
  assumes "x \<preceq> y in xs"
  shows "x \<preceq> y in (ys @ xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<preceq> y in (ys @ xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in xs

goal (1 subgoal):
 1. x \<preceq> y in (ys @ xs)
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l r. xs = l @ x # r \<and> y \<in> set (x # r)

goal (1 subgoal):
 1. \<exists>l r. ys @ xs = l @ x # r \<and> y \<in> set (x # r)
[PROOF STEP]
by (metis append.assoc)


[STATEMENT]
lemma precedes_append_left_iff:
  assumes "x \<notin> set ys"
  shows "x \<preceq> y in (ys @ xs) \<longleftrightarrow> x \<preceq> y in xs" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<preceq> y in (ys @ xs)) = (x \<preceq> y in xs)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<preceq> y in (ys @ xs) \<Longrightarrow> x \<preceq> y in xs
 2. x \<preceq> y in xs \<Longrightarrow> x \<preceq> y in (ys @ xs)
[PROOF STEP]
assume "?lhs"
[PROOF STATE]
proof (state)
this:
x \<preceq> y in (ys @ xs)

goal (2 subgoals):
 1. x \<preceq> y in (ys @ xs) \<Longrightarrow> x \<preceq> y in xs
 2. x \<preceq> y in xs \<Longrightarrow> x \<preceq> y in (ys @ xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<preceq> y in (ys @ xs)
[PROOF STEP]
obtain l r where lr: "ys @ xs = l @ (x # r)" "y \<in> set (x # r)"
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in (ys @ xs)

goal (1 subgoal):
 1. (\<And>l r. \<lbrakk>ys @ xs = l @ x # r; y \<in> set (x # r)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l r. ys @ xs = l @ x # r \<and> y \<in> set (x # r)

goal (1 subgoal):
 1. (\<And>l r. \<lbrakk>ys @ xs = l @ x # r; y \<in> set (x # r)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ys @ xs = l @ x # r
y \<in> set (x # r)

goal (2 subgoals):
 1. x \<preceq> y in (ys @ xs) \<Longrightarrow> x \<preceq> y in xs
 2. x \<preceq> y in xs \<Longrightarrow> x \<preceq> y in (ys @ xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys @ xs = l @ x # r
y \<in> set (x # r)
[PROOF STEP]
obtain us where
    "(ys = l @ us \<and> us @ xs = x # r) \<or> (ys @ us = l \<and> xs = us @ (x # r))"
[PROOF STATE]
proof (prove)
using this:
ys @ xs = l @ x # r
y \<in> set (x # r)

goal (1 subgoal):
 1. (\<And>us. ys = l @ us \<and> us @ xs = x # r \<or> ys @ us = l \<and> xs = us @ x # r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: append_eq_append_conv2)
[PROOF STATE]
proof (state)
this:
ys = l @ us \<and> us @ xs = x # r \<or> ys @ us = l \<and> xs = us @ x # r

goal (2 subgoals):
 1. x \<preceq> y in (ys @ xs) \<Longrightarrow> x \<preceq> y in xs
 2. x \<preceq> y in xs \<Longrightarrow> x \<preceq> y in (ys @ xs)
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
ys = l @ us \<and> us @ xs = x # r \<or> ys @ us = l \<and> xs = us @ x # r

goal (1 subgoal):
 1. x \<preceq> y in xs
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ys = l @ us \<and> us @ xs = x # r \<Longrightarrow> x \<preceq> y in xs
 2. ys @ us = l \<and> xs = us @ x # r \<Longrightarrow> x \<preceq> y in xs
[PROOF STEP]
assume us: "ys = l @ us \<and> us @ xs = x # r"
[PROOF STATE]
proof (state)
this:
ys = l @ us \<and> us @ xs = x # r

goal (2 subgoals):
 1. ys = l @ us \<and> us @ xs = x # r \<Longrightarrow> x \<preceq> y in xs
 2. ys @ us = l \<and> xs = us @ x # r \<Longrightarrow> x \<preceq> y in xs
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
x \<notin> set ys
ys = l @ us \<and> us @ xs = x # r
[PROOF STEP]
have "us = []"
[PROOF STATE]
proof (prove)
using this:
x \<notin> set ys
ys = l @ us \<and> us @ xs = x # r

goal (1 subgoal):
 1. us = []
[PROOF STEP]
by (metis Cons_eq_append_conv in_set_conv_decomp)
[PROOF STATE]
proof (state)
this:
us = []

goal (2 subgoals):
 1. ys = l @ us \<and> us @ xs = x # r \<Longrightarrow> x \<preceq> y in xs
 2. ys @ us = l \<and> xs = us @ x # r \<Longrightarrow> x \<preceq> y in xs
[PROOF STEP]
with us lr
[PROOF STATE]
proof (chain)
picking this:
ys = l @ us \<and> us @ xs = x # r
ys @ xs = l @ x # r
y \<in> set (x # r)
us = []
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
ys = l @ us \<and> us @ xs = x # r
ys @ xs = l @ x # r
y \<in> set (x # r)
us = []

goal (1 subgoal):
 1. x \<preceq> y in xs
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
ys = l @ us \<and> us @ xs = x # r
ys @ xs = l @ x # r
y \<in> set (x # r)
us = []

goal (1 subgoal):
 1. \<exists>l r. xs = l @ x # r \<and> y \<in> set (x # r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<preceq> y in xs

goal (1 subgoal):
 1. ys @ us = l \<and> xs = us @ x # r \<Longrightarrow> x \<preceq> y in xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ys @ us = l \<and> xs = us @ x # r \<Longrightarrow> x \<preceq> y in xs
[PROOF STEP]
assume us: "ys @ us = l \<and> xs = us @ (x # r)"
[PROOF STATE]
proof (state)
this:
ys @ us = l \<and> xs = us @ x # r

goal (1 subgoal):
 1. ys @ us = l \<and> xs = us @ x # r \<Longrightarrow> x \<preceq> y in xs
[PROOF STEP]
with \<open>y \<in> set (x # r)\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> set (x # r)
ys @ us = l \<and> xs = us @ x # r
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
y \<in> set (x # r)
ys @ us = l \<and> xs = us @ x # r

goal (1 subgoal):
 1. x \<preceq> y in xs
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
y \<in> set (x # r)
ys @ us = l \<and> xs = us @ x # r

goal (1 subgoal):
 1. \<exists>l r. xs = l @ x # r \<and> y \<in> set (x # r)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<preceq> y in xs

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

goal (1 subgoal):
 1. x \<preceq> y in xs \<Longrightarrow> x \<preceq> y in (ys @ xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<preceq> y in xs \<Longrightarrow> x \<preceq> y in (ys @ xs)
[PROOF STEP]
assume "?rhs"
[PROOF STATE]
proof (state)
this:
x \<preceq> y in xs

goal (1 subgoal):
 1. x \<preceq> y in xs \<Longrightarrow> x \<preceq> y in (ys @ xs)
[PROOF STEP]
thus "?lhs"
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in xs

goal (1 subgoal):
 1. x \<preceq> y in (ys @ xs)
[PROOF STEP]
by (rule precedes_append_left)
[PROOF STATE]
proof (state)
this:
x \<preceq> y in (ys @ xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma precedes_append_right:
  assumes "x \<preceq> y in xs"
  shows "x \<preceq> y in (xs @ ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<preceq> y in (xs @ ys)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in xs

goal (1 subgoal):
 1. x \<preceq> y in (xs @ ys)
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l r. xs = l @ x # r \<and> y \<in> set (x # r)

goal (1 subgoal):
 1. \<exists>l r. xs @ ys = l @ x # r \<and> y \<in> set (x # r)
[PROOF STEP]
by force


[STATEMENT]
lemma precedes_append_right_iff:
  assumes "y \<notin> set ys"
  shows "x \<preceq> y in (xs @ ys) \<longleftrightarrow> x \<preceq> y in xs" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<preceq> y in (xs @ ys)) = (x \<preceq> y in xs)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<preceq> y in (xs @ ys) \<Longrightarrow> x \<preceq> y in xs
 2. x \<preceq> y in xs \<Longrightarrow> x \<preceq> y in (xs @ ys)
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
x \<preceq> y in (xs @ ys)

goal (2 subgoals):
 1. x \<preceq> y in (xs @ ys) \<Longrightarrow> x \<preceq> y in xs
 2. x \<preceq> y in xs \<Longrightarrow> x \<preceq> y in (xs @ ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<preceq> y in (xs @ ys)
[PROOF STEP]
obtain l r where lr: "xs @ ys = l @ (x # r)" "y \<in> set (x # r)"
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in (xs @ ys)

goal (1 subgoal):
 1. (\<And>l r. \<lbrakk>xs @ ys = l @ x # r; y \<in> set (x # r)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l r. xs @ ys = l @ x # r \<and> y \<in> set (x # r)

goal (1 subgoal):
 1. (\<And>l r. \<lbrakk>xs @ ys = l @ x # r; y \<in> set (x # r)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xs @ ys = l @ x # r
y \<in> set (x # r)

goal (2 subgoals):
 1. x \<preceq> y in (xs @ ys) \<Longrightarrow> x \<preceq> y in xs
 2. x \<preceq> y in xs \<Longrightarrow> x \<preceq> y in (xs @ ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs @ ys = l @ x # r
y \<in> set (x # r)
[PROOF STEP]
obtain us where
    "(xs = l @ us \<and> us @ ys = x # r) \<or> (xs @ us = l \<and> ys = us @ (x # r))"
[PROOF STATE]
proof (prove)
using this:
xs @ ys = l @ x # r
y \<in> set (x # r)

goal (1 subgoal):
 1. (\<And>us. xs = l @ us \<and> us @ ys = x # r \<or> xs @ us = l \<and> ys = us @ x # r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: append_eq_append_conv2)
[PROOF STATE]
proof (state)
this:
xs = l @ us \<and> us @ ys = x # r \<or> xs @ us = l \<and> ys = us @ x # r

goal (2 subgoals):
 1. x \<preceq> y in (xs @ ys) \<Longrightarrow> x \<preceq> y in xs
 2. x \<preceq> y in xs \<Longrightarrow> x \<preceq> y in (xs @ ys)
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
xs = l @ us \<and> us @ ys = x # r \<or> xs @ us = l \<and> ys = us @ x # r

goal (1 subgoal):
 1. x \<preceq> y in xs
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = l @ us \<and> us @ ys = x # r \<Longrightarrow> x \<preceq> y in xs
 2. xs @ us = l \<and> ys = us @ x # r \<Longrightarrow> x \<preceq> y in xs
[PROOF STEP]
assume us: "xs = l @ us \<and> us @ ys = x # r"
[PROOF STATE]
proof (state)
this:
xs = l @ us \<and> us @ ys = x # r

goal (2 subgoals):
 1. xs = l @ us \<and> us @ ys = x # r \<Longrightarrow> x \<preceq> y in xs
 2. xs @ us = l \<and> ys = us @ x # r \<Longrightarrow> x \<preceq> y in xs
[PROOF STEP]
with \<open>y \<in> set (x # r)\<close> assms
[PROOF STATE]
proof (chain)
picking this:
y \<in> set (x # r)
y \<notin> set ys
xs = l @ us \<and> us @ ys = x # r
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
y \<in> set (x # r)
y \<notin> set ys
xs = l @ us \<and> us @ ys = x # r

goal (1 subgoal):
 1. x \<preceq> y in xs
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
y \<in> set (x # r)
y \<notin> set ys
xs = l @ us \<and> us @ ys = x # r

goal (1 subgoal):
 1. \<exists>l r. xs = l @ x # r \<and> y \<in> set (x # r)
[PROOF STEP]
by (metis Cons_eq_append_conv Un_iff set_append)
[PROOF STATE]
proof (state)
this:
x \<preceq> y in xs

goal (1 subgoal):
 1. xs @ us = l \<and> ys = us @ x # r \<Longrightarrow> x \<preceq> y in xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs @ us = l \<and> ys = us @ x # r \<Longrightarrow> x \<preceq> y in xs
[PROOF STEP]
assume us: "xs @ us = l \<and> ys = us @ (x # r)"
[PROOF STATE]
proof (state)
this:
xs @ us = l \<and> ys = us @ x # r

goal (1 subgoal):
 1. xs @ us = l \<and> ys = us @ x # r \<Longrightarrow> x \<preceq> y in xs
[PROOF STEP]
with \<open>y \<in> set (x # r)\<close> assms
[PROOF STATE]
proof (chain)
picking this:
y \<in> set (x # r)
y \<notin> set ys
xs @ us = l \<and> ys = us @ x # r
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
y \<in> set (x # r)
y \<notin> set ys
xs @ us = l \<and> ys = us @ x # r

goal (1 subgoal):
 1. x \<preceq> y in xs
[PROOF STEP]
by auto \<comment> \<open>contradiction\<close>
[PROOF STATE]
proof (state)
this:
x \<preceq> y in xs

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

goal (1 subgoal):
 1. x \<preceq> y in xs \<Longrightarrow> x \<preceq> y in (xs @ ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<preceq> y in xs \<Longrightarrow> x \<preceq> y in (xs @ ys)
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
x \<preceq> y in xs

goal (1 subgoal):
 1. x \<preceq> y in xs \<Longrightarrow> x \<preceq> y in (xs @ ys)
[PROOF STEP]
thus ?lhs
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in xs

goal (1 subgoal):
 1. x \<preceq> y in (xs @ ys)
[PROOF STEP]
by (rule precedes_append_right)
[PROOF STATE]
proof (state)
this:
x \<preceq> y in (xs @ ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma precedes_trans:
  assumes "x \<preceq> y in xs" and "y \<preceq> z in xs" and "distinct xs"
  shows "x \<preceq> z in xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<preceq> z in xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in xs
y \<preceq> z in xs
distinct xs

goal (1 subgoal):
 1. x \<preceq> z in xs
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l r. xs = l @ x # r \<and> y \<in> set (x # r)
\<exists>l r. xs = l @ y # r \<and> z \<in> set (y # r)
distinct xs

goal (1 subgoal):
 1. \<exists>l r. xs = l @ x # r \<and> z \<in> set (x # r)
[PROOF STEP]
by (smt Un_iff append.assoc append_Cons_eq_iff distinct_append
          not_distinct_conv_prefix set_append split_list_last)


[STATEMENT]
lemma precedes_antisym:
  assumes "x \<preceq> y in xs" and "y \<preceq> x in xs" and "distinct xs"
  shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
from \<open>x \<preceq> y in xs\<close> \<open>distinct xs\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<preceq> y in xs
distinct xs
[PROOF STEP]
obtain as bs where
    1: "xs = as @ (x # bs)" "y \<in> set (x # bs)" "y \<notin> set as"
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in xs
distinct xs

goal (1 subgoal):
 1. (\<And>as bs. \<lbrakk>xs = as @ x # bs; y \<in> set (x # bs); y \<notin> set as\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l r. xs = l @ x # r \<and> y \<in> set (x # r)
distinct xs

goal (1 subgoal):
 1. (\<And>as bs. \<lbrakk>xs = as @ x # bs; y \<in> set (x # bs); y \<notin> set as\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
xs = as @ x # bs
y \<in> set (x # bs)
y \<notin> set as

goal (1 subgoal):
 1. x = y
[PROOF STEP]
from \<open>y \<preceq> x in xs\<close> \<open>distinct xs\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<preceq> x in xs
distinct xs
[PROOF STEP]
obtain cs ds where
    2: "xs = cs @ (y # ds)" "x \<in> set (y # ds)" "x \<notin> set cs"
[PROOF STATE]
proof (prove)
using this:
y \<preceq> x in xs
distinct xs

goal (1 subgoal):
 1. (\<And>cs ds. \<lbrakk>xs = cs @ y # ds; x \<in> set (y # ds); x \<notin> set cs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l r. xs = l @ y # r \<and> x \<in> set (y # r)
distinct xs

goal (1 subgoal):
 1. (\<And>cs ds. \<lbrakk>xs = cs @ y # ds; x \<in> set (y # ds); x \<notin> set cs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
xs = cs @ y # ds
x \<in> set (y # ds)
x \<notin> set cs

goal (1 subgoal):
 1. x = y
[PROOF STEP]
from 1 2
[PROOF STATE]
proof (chain)
picking this:
xs = as @ x # bs
y \<in> set (x # bs)
y \<notin> set as
xs = cs @ y # ds
x \<in> set (y # ds)
x \<notin> set cs
[PROOF STEP]
have "as @ (x # bs) = cs @ (y # ds)"
[PROOF STATE]
proof (prove)
using this:
xs = as @ x # bs
y \<in> set (x # bs)
y \<notin> set as
xs = cs @ y # ds
x \<in> set (y # ds)
x \<notin> set cs

goal (1 subgoal):
 1. as @ x # bs = cs @ y # ds
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
as @ x # bs = cs @ y # ds

goal (1 subgoal):
 1. x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
as @ x # bs = cs @ y # ds
[PROOF STEP]
obtain zs where
    "(as = cs @ zs \<and> zs @ (x # bs) = y # ds)
     \<or> (as @ zs = cs \<and> x # bs = zs @ (y # ds))"  (is "?P \<or> ?Q")
[PROOF STATE]
proof (prove)
using this:
as @ x # bs = cs @ y # ds

goal (1 subgoal):
 1. (\<And>zs. as = cs @ zs \<and> zs @ x # bs = y # ds \<or> as @ zs = cs \<and> x # bs = zs @ y # ds \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: append_eq_append_conv2)
[PROOF STATE]
proof (state)
this:
as = cs @ zs \<and> zs @ x # bs = y # ds \<or> as @ zs = cs \<and> x # bs = zs @ y # ds

goal (1 subgoal):
 1. x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
as = cs @ zs \<and> zs @ x # bs = y # ds \<or> as @ zs = cs \<and> x # bs = zs @ y # ds
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as = cs @ zs \<and> zs @ x # bs = y # ds \<or> as @ zs = cs \<and> x # bs = zs @ y # ds

goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. as = cs @ zs \<and> zs @ x # bs = y # ds \<Longrightarrow> x = y
 2. as @ zs = cs \<and> x # bs = zs @ y # ds \<Longrightarrow> x = y
[PROOF STEP]
assume "?P"
[PROOF STATE]
proof (state)
this:
as = cs @ zs \<and> zs @ x # bs = y # ds

goal (2 subgoals):
 1. as = cs @ zs \<and> zs @ x # bs = y # ds \<Longrightarrow> x = y
 2. as @ zs = cs \<and> x # bs = zs @ y # ds \<Longrightarrow> x = y
[PROOF STEP]
with \<open>y \<notin> set as\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<notin> set as
as = cs @ zs \<and> zs @ x # bs = y # ds
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<notin> set as
as = cs @ zs \<and> zs @ x # bs = y # ds

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (cases "zs") auto
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. as @ zs = cs \<and> x # bs = zs @ y # ds \<Longrightarrow> x = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. as @ zs = cs \<and> x # bs = zs @ y # ds \<Longrightarrow> x = y
[PROOF STEP]
assume "?Q"
[PROOF STATE]
proof (state)
this:
as @ zs = cs \<and> x # bs = zs @ y # ds

goal (1 subgoal):
 1. as @ zs = cs \<and> x # bs = zs @ y # ds \<Longrightarrow> x = y
[PROOF STEP]
with \<open>x \<notin> set cs\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<notin> set cs
as @ zs = cs \<and> x # bs = zs @ y # ds
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<notin> set cs
as @ zs = cs \<and> x # bs = zs @ y # ds

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (cases "zs") auto
[PROOF STATE]
proof (state)
this:
x = y

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reachable_edge: "edge x y \<Longrightarrow> reachable x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edge x y \<Longrightarrow> reachable x y
[PROOF STEP]
by auto


[STATEMENT]
lemma succ_reachable:
  assumes "reachable x y" and "edge y z"
  shows "reachable x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable x z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachable x y
edge y z

goal (1 subgoal):
 1. reachable x z
[PROOF STEP]
by induct auto


[STATEMENT]
lemma reachable_trans:
  assumes y: "reachable x y" and z: "reachable y z"
  shows "reachable x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable x z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachable x y
reachable y z

goal (1 subgoal):
 1. reachable x z
[PROOF STEP]
by induct auto


[STATEMENT]
lemma succ_re:
  assumes y: "edge x y" and z: "reachable_end y z"
  shows "reachable_end x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_end x z
[PROOF STEP]
using z y
[PROOF STATE]
proof (prove)
using this:
reachable_end y z
edge x y

goal (1 subgoal):
 1. reachable_end x z
[PROOF STEP]
by (induction) (auto intro: re_succ)


[STATEMENT]
lemma reachable_re:
  assumes "reachable x y"
  shows "reachable_end x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_end x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachable x y

goal (1 subgoal):
 1. reachable_end x y
[PROOF STEP]
by (induction) (auto intro: succ_re)


[STATEMENT]
lemma re_reachable:
  assumes "reachable_end x y"
  shows "reachable x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachable_end x y

goal (1 subgoal):
 1. reachable x y
[PROOF STEP]
by (induction) (auto intro: succ_reachable)


[STATEMENT]
lemma reachable_end_induct:
  assumes r: "reachable x y"
      and base: "\<And>x. P x x"
      and step: "\<And>x y z. \<lbrakk>P x y; edge y z\<rbrakk> \<Longrightarrow> P x z"
  shows "P x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P x y
[PROOF STEP]
using r[THEN reachable_re]
[PROOF STATE]
proof (prove)
using this:
reachable_end x y

goal (1 subgoal):
 1. P x y
[PROOF STEP]
proof (induction)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. P x x
 2. \<And>x y z. \<lbrakk>reachable_end x y; P x y; edge y z\<rbrakk> \<Longrightarrow> P x z
[PROOF STEP]
case (re_refl x)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x. P x x
 2. \<And>x y z. \<lbrakk>reachable_end x y; P x y; edge y z\<rbrakk> \<Longrightarrow> P x z
[PROOF STEP]
from base
[PROOF STATE]
proof (chain)
picking this:
P ?x ?x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P ?x ?x

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

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>reachable_end x y; P x y; edge y z\<rbrakk> \<Longrightarrow> P x z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>reachable_end x y; P x y; edge y z\<rbrakk> \<Longrightarrow> P x z
[PROOF STEP]
case (re_succ x y z)
[PROOF STATE]
proof (state)
this:
reachable_end x y
edge y z
P x y

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>reachable_end x y; P x y; edge y z\<rbrakk> \<Longrightarrow> P x z
[PROOF STEP]
with step
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>P ?x ?y; edge ?y ?z\<rbrakk> \<Longrightarrow> P ?x ?z
reachable_end x y
edge y z
P x y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P ?x ?y; edge ?y ?z\<rbrakk> \<Longrightarrow> P ?x ?z
reachable_end x y
edge y z
P x y

goal (1 subgoal):
 1. P x z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P x z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma edge_ra:
  assumes "edge x y" and "(x,y) \<notin> E"
  shows "reachable_avoiding x y E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_avoiding x y E
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
edge x y
(x, y) \<notin> E

goal (1 subgoal):
 1. reachable_avoiding x y E
[PROOF STEP]
by (meson reachable_avoiding.simps)


[STATEMENT]
lemma ra_trans:
  assumes 1: "reachable_avoiding x y E" and 2: "reachable_avoiding y z E"
  shows "reachable_avoiding x z E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_avoiding x z E
[PROOF STEP]
using 2 1
[PROOF STATE]
proof (prove)
using this:
reachable_avoiding y z E
reachable_avoiding x y E

goal (1 subgoal):
 1. reachable_avoiding x z E
[PROOF STEP]
by induction auto


[STATEMENT]
lemma ra_cases:
  assumes "reachable_avoiding x y E"
  shows "x=y \<or> (\<exists>z. z \<in> successors x \<and> (x,z) \<notin> E \<and> reachable_avoiding z y E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y \<or> (\<exists>z. edge x z \<and> (x, z) \<notin> E \<and> reachable_avoiding z y E)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachable_avoiding x y E

goal (1 subgoal):
 1. x = y \<or> (\<exists>z. edge x z \<and> (x, z) \<notin> E \<and> reachable_avoiding z y E)
[PROOF STEP]
proof (induction)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x E. x = x \<or> (\<exists>z. edge x z \<and> (x, z) \<notin> E \<and> reachable_avoiding z x E)
 2. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; x = y \<or> (\<exists>z. edge x z \<and> (x, z) \<notin> E \<and> reachable_avoiding z y E); edge y z; (y, z) \<notin> E\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>za. edge x za \<and> (x, za) \<notin> E \<and> reachable_avoiding za z E)
[PROOF STEP]
case (ra_refl x S)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x E. x = x \<or> (\<exists>z. edge x z \<and> (x, z) \<notin> E \<and> reachable_avoiding z x E)
 2. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; x = y \<or> (\<exists>z. edge x z \<and> (x, z) \<notin> E \<and> reachable_avoiding z y E); edge y z; (y, z) \<notin> E\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>za. edge x za \<and> (x, za) \<notin> E \<and> reachable_avoiding za z E)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x \<or> (\<exists>z. edge x z \<and> (x, z) \<notin> S \<and> reachable_avoiding z x S)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = x \<or> (\<exists>z. edge x z \<and> (x, z) \<notin> S \<and> reachable_avoiding z x S)

goal (1 subgoal):
 1. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; x = y \<or> (\<exists>z. edge x z \<and> (x, z) \<notin> E \<and> reachable_avoiding z y E); edge y z; (y, z) \<notin> E\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>za. edge x za \<and> (x, za) \<notin> E \<and> reachable_avoiding za z E)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; x = y \<or> (\<exists>z. edge x z \<and> (x, z) \<notin> E \<and> reachable_avoiding z y E); edge y z; (y, z) \<notin> E\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>za. edge x za \<and> (x, za) \<notin> E \<and> reachable_avoiding za z E)
[PROOF STEP]
case (ra_succ x y S z)
[PROOF STATE]
proof (state)
this:
reachable_avoiding x y S
edge y z
(y, z) \<notin> S
x = y \<or> (\<exists>z. edge x z \<and> (x, z) \<notin> S \<and> reachable_avoiding z y S)

goal (1 subgoal):
 1. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; x = y \<or> (\<exists>z. edge x z \<and> (x, z) \<notin> E \<and> reachable_avoiding z y E); edge y z; (y, z) \<notin> E\<rbrakk> \<Longrightarrow> x = z \<or> (\<exists>za. edge x za \<and> (x, za) \<notin> E \<and> reachable_avoiding za z E)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
reachable_avoiding x y S
edge y z
(y, z) \<notin> S
x = y \<or> (\<exists>z. edge x z \<and> (x, z) \<notin> S \<and> reachable_avoiding z y S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
reachable_avoiding x y S
edge y z
(y, z) \<notin> S
x = y \<or> (\<exists>z. edge x z \<and> (x, z) \<notin> S \<and> reachable_avoiding z y S)

goal (1 subgoal):
 1. x = z \<or> (\<exists>za. edge x za \<and> (x, za) \<notin> S \<and> reachable_avoiding za z S)
[PROOF STEP]
by (metis ra_refl reachable_avoiding.ra_succ)
[PROOF STATE]
proof (state)
this:
x = z \<or> (\<exists>za. edge x za \<and> (x, za) \<notin> S \<and> reachable_avoiding za z S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ra_mono:
  assumes "reachable_avoiding x y E" and "E' \<subseteq> E"
  shows "reachable_avoiding x y E'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_avoiding x y E'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachable_avoiding x y E
E' \<subseteq> E

goal (1 subgoal):
 1. reachable_avoiding x y E'
[PROOF STEP]
by induction auto


[STATEMENT]
lemma ra_add_edge:
  assumes "reachable_avoiding x y E"
  shows "reachable_avoiding x y (E \<union> {(v,w)})
         \<or> (reachable_avoiding x v (E \<union> {(v,w)}) \<and> reachable_avoiding w y (E \<union> {(v,w)}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_avoiding x y (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w y (E \<union> {(v, w)})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachable_avoiding x y E

goal (1 subgoal):
 1. reachable_avoiding x y (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w y (E \<union> {(v, w)})
[PROOF STEP]
proof (induction)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x E. reachable_avoiding x x (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w x (E \<union> {(v, w)})
 2. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; reachable_avoiding x y (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w y (E \<union> {(v, w)}); edge y z; (y, z) \<notin> E\<rbrakk> \<Longrightarrow> reachable_avoiding x z (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w z (E \<union> {(v, w)})
[PROOF STEP]
case (ra_refl x E)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x E. reachable_avoiding x x (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w x (E \<union> {(v, w)})
 2. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; reachable_avoiding x y (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w y (E \<union> {(v, w)}); edge y z; (y, z) \<notin> E\<rbrakk> \<Longrightarrow> reachable_avoiding x z (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w z (E \<union> {(v, w)})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_avoiding x x (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w x (E \<union> {(v, w)})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
reachable_avoiding x x (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w x (E \<union> {(v, w)})

goal (1 subgoal):
 1. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; reachable_avoiding x y (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w y (E \<union> {(v, w)}); edge y z; (y, z) \<notin> E\<rbrakk> \<Longrightarrow> reachable_avoiding x z (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w z (E \<union> {(v, w)})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; reachable_avoiding x y (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w y (E \<union> {(v, w)}); edge y z; (y, z) \<notin> E\<rbrakk> \<Longrightarrow> reachable_avoiding x z (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w z (E \<union> {(v, w)})
[PROOF STEP]
case (ra_succ x y E z)
[PROOF STATE]
proof (state)
this:
reachable_avoiding x y E
edge y z
(y, z) \<notin> E
reachable_avoiding x y (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w y (E \<union> {(v, w)})

goal (1 subgoal):
 1. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; reachable_avoiding x y (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w y (E \<union> {(v, w)}); edge y z; (y, z) \<notin> E\<rbrakk> \<Longrightarrow> reachable_avoiding x z (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w z (E \<union> {(v, w)})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
reachable_avoiding x y E
edge y z
(y, z) \<notin> E
reachable_avoiding x y (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w y (E \<union> {(v, w)})
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
reachable_avoiding x y E
edge y z
(y, z) \<notin> E
reachable_avoiding x y (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w y (E \<union> {(v, w)})

goal (1 subgoal):
 1. reachable_avoiding x z (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w z (E \<union> {(v, w)})
[PROOF STEP]
using reachable_avoiding.ra_succ
[PROOF STATE]
proof (prove)
using this:
reachable_avoiding x y E
edge y z
(y, z) \<notin> E
reachable_avoiding x y (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w y (E \<union> {(v, w)})
\<lbrakk>reachable_avoiding ?x ?y ?E; edge ?y ?z; (?y, ?z) \<notin> ?E\<rbrakk> \<Longrightarrow> reachable_avoiding ?x ?z ?E

goal (1 subgoal):
 1. reachable_avoiding x z (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w z (E \<union> {(v, w)})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reachable_avoiding x z (E \<union> {(v, w)}) \<or> reachable_avoiding x v (E \<union> {(v, w)}) \<and> reachable_avoiding w z (E \<union> {(v, w)})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ra_reachable:
  "reachable_avoiding x y E \<Longrightarrow> reachable x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_avoiding x y E \<Longrightarrow> reachable x y
[PROOF STEP]
by (induction rule: reachable_avoiding.induct) (auto intro: succ_reachable)


[STATEMENT]
lemma ra_empty:
  "reachable_avoiding x y {} = reachable x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_avoiding x y {} = reachable x y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. reachable_avoiding x y {} \<Longrightarrow> reachable x y
 2. reachable x y \<Longrightarrow> reachable_avoiding x y {}
[PROOF STEP]
assume "reachable_avoiding x y {}"
[PROOF STATE]
proof (state)
this:
reachable_avoiding x y {}

goal (2 subgoals):
 1. reachable_avoiding x y {} \<Longrightarrow> reachable x y
 2. reachable x y \<Longrightarrow> reachable_avoiding x y {}
[PROOF STEP]
thus "reachable x y"
[PROOF STATE]
proof (prove)
using this:
reachable_avoiding x y {}

goal (1 subgoal):
 1. reachable x y
[PROOF STEP]
by (rule ra_reachable)
[PROOF STATE]
proof (state)
this:
reachable x y

goal (1 subgoal):
 1. reachable x y \<Longrightarrow> reachable_avoiding x y {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. reachable x y \<Longrightarrow> reachable_avoiding x y {}
[PROOF STEP]
assume "reachable x y"
[PROOF STATE]
proof (state)
this:
reachable x y

goal (1 subgoal):
 1. reachable x y \<Longrightarrow> reachable_avoiding x y {}
[PROOF STEP]
hence "reachable_end x y"
[PROOF STATE]
proof (prove)
using this:
reachable x y

goal (1 subgoal):
 1. reachable_end x y
[PROOF STEP]
by (rule reachable_re)
[PROOF STATE]
proof (state)
this:
reachable_end x y

goal (1 subgoal):
 1. reachable x y \<Longrightarrow> reachable_avoiding x y {}
[PROOF STEP]
thus "reachable_avoiding x y {}"
[PROOF STATE]
proof (prove)
using this:
reachable_end x y

goal (1 subgoal):
 1. reachable_avoiding x y {}
[PROOF STEP]
by induction auto
[PROOF STATE]
proof (state)
this:
reachable_avoiding x y {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subscc_add:
  assumes "is_subscc S" and "x \<in> S"
      and "reachable x y" and "reachable y x"
  shows "is_subscc (insert y S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_subscc (insert y S)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_subscc S
x \<in> S
reachable x y
reachable y x

goal (1 subgoal):
 1. is_subscc (insert y S)
[PROOF STEP]
unfolding is_subscc_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. \<forall>y\<in>S. reachable x y
x \<in> S
reachable x y
reachable y x

goal (1 subgoal):
 1. \<forall>x\<in>insert y S. \<forall>y\<in>insert y S. reachable x y
[PROOF STEP]
by (metis insert_iff reachable_trans)


[STATEMENT]
lemma sccE:
  \<comment> \<open>Two nodes that are reachable from each other are in the same SCC.\<close>
  assumes "is_scc S" and "x \<in> S"
      and "reachable x y" and "reachable y x"
  shows "y \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_scc S
x \<in> S
reachable x y
reachable y x

goal (1 subgoal):
 1. y \<in> S
[PROOF STEP]
unfolding is_scc_def
[PROOF STATE]
proof (prove)
using this:
S \<noteq> {} \<and> is_subscc S \<and> (\<forall>S'. S \<subseteq> S' \<and> is_subscc S' \<longrightarrow> S' = S)
x \<in> S
reachable x y
reachable y x

goal (1 subgoal):
 1. y \<in> S
[PROOF STEP]
by (metis insertI1 subscc_add subset_insertI)


[STATEMENT]
lemma scc_partition:
  \<comment> \<open>Two SCCs that contain a common element are identical.\<close>
  assumes "is_scc S" and "is_scc S'" and "x \<in> S \<inter> S'"
  shows "S = S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S = S'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_scc S
is_scc S'
x \<in> S \<inter> S'

goal (1 subgoal):
 1. S = S'
[PROOF STEP]
unfolding is_scc_def is_subscc_def
[PROOF STATE]
proof (prove)
using this:
S \<noteq> {} \<and> (\<forall>x\<in>S. \<forall>y\<in>S. reachable x y) \<and> (\<forall>S'. S \<subseteq> S' \<and> (\<forall>x\<in>S'. \<forall>y\<in>S'. reachable x y) \<longrightarrow> S' = S)
S' \<noteq> {} \<and> (\<forall>x\<in>S'. \<forall>y\<in>S'. reachable x y) \<and> (\<forall>S'a. S' \<subseteq> S'a \<and> (\<forall>x\<in>S'a. \<forall>y\<in>S'a. reachable x y) \<longrightarrow> S'a = S')
x \<in> S \<inter> S'

goal (1 subgoal):
 1. S = S'
[PROOF STEP]
by (metis IntE assms(2) sccE subsetI)


[STATEMENT]
lemma stack_visited:
  assumes "wf_env e" "n \<in> set (stack e)"
  shows "n \<in> visited e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> visited e
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_env e
n \<in> set (stack e)

goal (1 subgoal):
 1. n \<in> visited e
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>n\<in>visited e. reachable (root e) n) \<and> distinct (stack e) \<and> distinct (cstack e) \<and> (\<forall>n m. n \<preceq> m in stack e \<longrightarrow> n \<preceq> m in cstack e) \<and> (\<forall>n m. n \<preceq> m in stack e \<longrightarrow> reachable m n) \<and> explored e \<subseteq> visited e \<and> set (cstack e) \<subseteq> visited e \<and> (\<forall>n\<in>explored e. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e) \<and> (\<forall>n. vsuccs e n \<subseteq> successors n \<inter> visited e) \<and> (\<forall>n. n \<notin> visited e \<longrightarrow> vsuccs e n = {}) \<and> (\<forall>n\<in>explored e. vsuccs e n = successors n) \<and> (\<forall>n\<in>visited e - set (cstack e). vsuccs e n = successors n) \<and> (\<forall>n m. (m \<in> \<S> e n) = (\<S> e n = \<S> e m)) \<and> (\<forall>n. n \<notin> visited e \<longrightarrow> \<S> e n = {n}) \<and> (\<forall>n\<in>set (stack e). \<forall>m\<in>set (stack e). n \<noteq> m \<longrightarrow> \<S> e n \<inter> \<S> e m = {}) \<and> \<Union> {\<S> e n |n. n \<in> set (stack e)} = visited e - explored e \<and> (\<forall>n\<in>set (stack e). \<forall>m\<in>\<S> e n. m \<in> set (cstack e) \<longrightarrow> m \<preceq> n in cstack e) \<and> (\<forall>n m. n \<preceq> m in stack e \<and> n \<noteq> m \<longrightarrow> (\<forall>u\<in>\<S> e n. \<not> reachable_avoiding u m (unvisited e n))) \<and> (\<forall>n. is_subscc (\<S> e n)) \<and> Ball (sccs e) is_scc \<and> \<Union> (sccs e) = explored e
n \<in> set (stack e)

goal (1 subgoal):
 1. n \<in> visited e
[PROOF STEP]
by (meson precedes_refl subset_iff)


[STATEMENT]
lemma stack_class:
  assumes "wf_env e" "n \<in> set (stack e)" "m \<in> \<S> e n"
  shows "m \<in> visited e - explored e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in> visited e - explored e
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_env e
n \<in> set (stack e)
m \<in> \<S> e n

goal (1 subgoal):
 1. m \<in> visited e - explored e
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>n\<in>visited e. reachable (root e) n) \<and> distinct (stack e) \<and> distinct (cstack e) \<and> (\<forall>n m. n \<preceq> m in stack e \<longrightarrow> n \<preceq> m in cstack e) \<and> (\<forall>n m. n \<preceq> m in stack e \<longrightarrow> reachable m n) \<and> explored e \<subseteq> visited e \<and> set (cstack e) \<subseteq> visited e \<and> (\<forall>n\<in>explored e. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e) \<and> (\<forall>n. vsuccs e n \<subseteq> successors n \<inter> visited e) \<and> (\<forall>n. n \<notin> visited e \<longrightarrow> vsuccs e n = {}) \<and> (\<forall>n\<in>explored e. vsuccs e n = successors n) \<and> (\<forall>n\<in>visited e - set (cstack e). vsuccs e n = successors n) \<and> (\<forall>n m. (m \<in> \<S> e n) = (\<S> e n = \<S> e m)) \<and> (\<forall>n. n \<notin> visited e \<longrightarrow> \<S> e n = {n}) \<and> (\<forall>n\<in>set (stack e). \<forall>m\<in>set (stack e). n \<noteq> m \<longrightarrow> \<S> e n \<inter> \<S> e m = {}) \<and> \<Union> {\<S> e n |n. n \<in> set (stack e)} = visited e - explored e \<and> (\<forall>n\<in>set (stack e). \<forall>m\<in>\<S> e n. m \<in> set (cstack e) \<longrightarrow> m \<preceq> n in cstack e) \<and> (\<forall>n m. n \<preceq> m in stack e \<and> n \<noteq> m \<longrightarrow> (\<forall>u\<in>\<S> e n. \<not> reachable_avoiding u m (unvisited e n))) \<and> (\<forall>n. is_subscc (\<S> e n)) \<and> Ball (sccs e) is_scc \<and> \<Union> (sccs e) = explored e
n \<in> set (stack e)
m \<in> \<S> e n

goal (1 subgoal):
 1. m \<in> visited e - explored e
[PROOF STEP]
by blast


[STATEMENT]
lemma visited_unexplored:
  assumes "wf_env e" "m \<in> visited e" "m \<notin> explored e"
  obtains n where "n \<in> set (stack e)" "m \<in> \<S> e n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>n \<in> set (stack e); m \<in> \<S> e n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_env e
m \<in> visited e
m \<notin> explored e

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>n \<in> set (stack e); m \<in> \<S> e n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>n\<in>visited e. reachable (root e) n) \<and> distinct (stack e) \<and> distinct (cstack e) \<and> (\<forall>n m. n \<preceq> m in stack e \<longrightarrow> n \<preceq> m in cstack e) \<and> (\<forall>n m. n \<preceq> m in stack e \<longrightarrow> reachable m n) \<and> explored e \<subseteq> visited e \<and> set (cstack e) \<subseteq> visited e \<and> (\<forall>n\<in>explored e. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e) \<and> (\<forall>n. vsuccs e n \<subseteq> successors n \<inter> visited e) \<and> (\<forall>n. n \<notin> visited e \<longrightarrow> vsuccs e n = {}) \<and> (\<forall>n\<in>explored e. vsuccs e n = successors n) \<and> (\<forall>n\<in>visited e - set (cstack e). vsuccs e n = successors n) \<and> (\<forall>n m. (m \<in> \<S> e n) = (\<S> e n = \<S> e m)) \<and> (\<forall>n. n \<notin> visited e \<longrightarrow> \<S> e n = {n}) \<and> (\<forall>n\<in>set (stack e). \<forall>m\<in>set (stack e). n \<noteq> m \<longrightarrow> \<S> e n \<inter> \<S> e m = {}) \<and> \<Union> {\<S> e n |n. n \<in> set (stack e)} = visited e - explored e \<and> (\<forall>n\<in>set (stack e). \<forall>m\<in>\<S> e n. m \<in> set (cstack e) \<longrightarrow> m \<preceq> n in cstack e) \<and> (\<forall>n m. n \<preceq> m in stack e \<and> n \<noteq> m \<longrightarrow> (\<forall>u\<in>\<S> e n. \<not> reachable_avoiding u m (unvisited e n))) \<and> (\<forall>n. is_subscc (\<S> e n)) \<and> Ball (sccs e) is_scc \<and> \<Union> (sccs e) = explored e
m \<in> visited e
m \<notin> explored e

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>n \<in> set (stack e); m \<in> \<S> e n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (smt (verit, ccfv_threshold) Diff_iff Union_iff mem_Collect_eq)


[STATEMENT]
lemma S_reflexive:
  assumes "wf_env e"
  shows "n \<in> \<S> e n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> \<S> e n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_env e

goal (1 subgoal):
 1. n \<in> \<S> e n
[PROOF STEP]
by (auto simp: wf_env_def)


[STATEMENT]
lemma stack_unexplored:
  assumes 1: "wf_env e"
      and 2: "n \<in> set (stack e)"
      and 3: "n \<in> explored e"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using stack_class[OF 1 2] S_reflexive[OF 1] 3
[PROOF STATE]
proof (prove)
using this:
?m \<in> \<S> e n \<Longrightarrow> ?m \<in> visited e - explored e
?n \<in> \<S> e ?n
n \<in> explored e

goal (1 subgoal):
 1. P
[PROOF STEP]
by blast