[STATEMENT]
theorem closure_sound_complete:
assumes result: "closure as (r,s) = Some(ws,R)"
and atoms: "set as = atoms r \<union> atoms s"
shows "ws = [] \<longleftrightarrow> lang r = lang s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ws = []) = (lang r = lang s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (ws = []) = (lang r = lang s)
[PROOF STEP]
have leq: "(lang r = lang s) =
  (\<forall>(r',s') \<in> {((r0,s0),(nderiv a r0,nderiv a s0))| r0 s0 a. a : set as}^* `` {(r,s)}.
    nullable r' = nullable s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lang r = lang s) = (\<forall>(r', s')\<in>{((r0, s0), nderiv a r0, nderiv a s0) |r0 s0 a. a \<in> set as}\<^sup>* `` {(r, s)}. nullable r' = nullable s')
[PROOF STEP]
by(simp add: atoms rtrancl_nderiv_nderivs Ball_def lang_eq_ext imp_ex nullable_nderivs
         del:Un_iff)
[PROOF STATE]
proof (state)
this:
(lang r = lang s) = (\<forall>(r', s')\<in>{((r0, s0), nderiv a r0, nderiv a s0) |r0 s0 a. a \<in> set as}\<^sup>* `` {(r, s)}. nullable r' = nullable s')

goal (1 subgoal):
 1. (ws = []) = (lang r = lang s)
[PROOF STEP]
have "{(x,y). y \<in> set ((\<lambda>(p,q). map (\<lambda>a. (nderiv a p, nderiv a q)) as) x)} =
    {((r,s), nderiv a r, nderiv a s) |r s a. a \<in> set as}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). y \<in> set (case x of (p, q) \<Rightarrow> map (\<lambda>a. (nderiv a p, nderiv a q)) as)} = {((r, s), nderiv a r, nderiv a s) |r s a. a \<in> set as}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). y \<in> set (case x of (p, q) \<Rightarrow> map (\<lambda>a. (nderiv a p, nderiv a q)) as)} = {((r, s), nderiv a r, nderiv a s) |r s a. a \<in> set as}

goal (1 subgoal):
 1. (ws = []) = (lang r = lang s)
[PROOF STEP]
with atoms rtrancl_while_Some[OF result[unfolded closure_def]]
[PROOF STATE]
proof (chain)
picking this:
set as = atoms r \<union> atoms s
if ws = [] then R = {(x, y). y \<in> set (case x of (r, s) \<Rightarrow> map (\<lambda>a. (nderiv a r, nderiv a s)) as)}\<^sup>* `` {(r, s)} \<and> (\<forall>z\<in>R. case z of (r, s) \<Rightarrow> nullable r = nullable s) else \<not> (case hd ws of (r, s) \<Rightarrow> nullable r = nullable s) \<and> hd ws \<in> {(x, y). y \<in> set (case x of (r, s) \<Rightarrow> map (\<lambda>a. (nderiv a r, nderiv a s)) as)}\<^sup>* `` {(r, s)}
{(x, y). y \<in> set (case x of (p, q) \<Rightarrow> map (\<lambda>a. (nderiv a p, nderiv a q)) as)} = {((r, s), nderiv a r, nderiv a s) |r s a. a \<in> set as}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set as = atoms r \<union> atoms s
if ws = [] then R = {(x, y). y \<in> set (case x of (r, s) \<Rightarrow> map (\<lambda>a. (nderiv a r, nderiv a s)) as)}\<^sup>* `` {(r, s)} \<and> (\<forall>z\<in>R. case z of (r, s) \<Rightarrow> nullable r = nullable s) else \<not> (case hd ws of (r, s) \<Rightarrow> nullable r = nullable s) \<and> hd ws \<in> {(x, y). y \<in> set (case x of (r, s) \<Rightarrow> map (\<lambda>a. (nderiv a r, nderiv a s)) as)}\<^sup>* `` {(r, s)}
{(x, y). y \<in> set (case x of (p, q) \<Rightarrow> map (\<lambda>a. (nderiv a p, nderiv a q)) as)} = {((r, s), nderiv a r, nderiv a s) |r s a. a \<in> set as}

goal (1 subgoal):
 1. (ws = []) = (lang r = lang s)
[PROOF STEP]
by (auto simp add: leq Ball_def split: if_splits)
[PROOF STATE]
proof (state)
this:
(ws = []) = (lang r = lang s)

goal:
No subgoals!
[PROOF STEP]
qed