[STATEMENT]
lemma steps_star_cycle[rule_format]:
 "us \<noteq> [] \<longrightarrow> (\<forall>u \<in> set us. accepts A u) \<longrightarrow> accepts (plus A) (concat us)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. accepts A u) \<longrightarrow> accepts (RegExp2NA.plus A) (concat us)
[PROOF STEP]
apply (simp add: accepts_conv_steps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q)
[PROOF STEP]
apply (induct us rule: rev_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. [] \<noteq> [] \<longrightarrow> (\<forall>u\<in>set []. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat []) \<and> fin A q)
 2. \<And>x xs. xs \<noteq> [] \<longrightarrow> (\<forall>u\<in>set xs. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat xs) \<and> fin A q) \<Longrightarrow> xs @ [x] \<noteq> [] \<longrightarrow> (\<forall>u\<in>set (xs @ [x]). \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat (xs @ [x])) \<and> fin A q)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. xs \<noteq> [] \<longrightarrow> (\<forall>u\<in>set xs. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat xs) \<and> fin A q) \<Longrightarrow> xs @ [x] \<noteq> [] \<longrightarrow> (\<forall>u\<in>set (xs @ [x]). \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat (xs @ [x])) \<and> fin A q)
[PROOF STEP]
apply (rename_tac u us)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u us. us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q) \<Longrightarrow> us @ [u] \<noteq> [] \<longrightarrow> (\<forall>u\<in>set (us @ [u]). \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat (us @ [u])) \<and> fin A q)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u us. us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q) \<Longrightarrow> (\<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<and> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q)
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u us q. \<lbrakk>us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q); \<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (case_tac "us = []")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>u us q. \<lbrakk>us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q); \<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us = []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
 2. \<And>u us q. \<lbrakk>us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q); \<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>u us q. \<lbrakk>(start A, q) \<in> steps A u; fin A q; us = []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) u \<and> fin A q
 2. \<And>u us q. \<lbrakk>us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q); \<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (blast intro: steps_plusI fin_steps_plusI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u us q. \<lbrakk>us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q); \<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u us q qa. \<lbrakk>\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []; (start A, qa) \<in> steps (RegExp2NA.plus A) (concat us); fin A qa\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (case_tac "u = []")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>u us q qa. \<lbrakk>\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []; (start A, qa) \<in> steps (RegExp2NA.plus A) (concat us); fin A qa; u = []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
 2. \<And>u us q qa. \<lbrakk>\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []; (start A, qa) \<in> steps (RegExp2NA.plus A) (concat us); fin A qa; u \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>u us q qa. \<lbrakk>\<forall>u\<in>set us. \<exists>qa. (q, qa) \<in> steps A u \<and> fin A qa; start A = q; fin A q; us \<noteq> []; (q, qa) \<in> steps (RegExp2NA.plus A) (concat us); fin A qa; u = []\<rbrakk> \<Longrightarrow> \<exists>qa. (q, qa) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A qa
 2. \<And>u us q qa. \<lbrakk>\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []; (start A, qa) \<in> steps (RegExp2NA.plus A) (concat us); fin A qa; u \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (blast intro: steps_plusI fin_steps_plusI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u us q qa. \<lbrakk>\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []; (start A, qa) \<in> steps (RegExp2NA.plus A) (concat us); fin A qa; u \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (blast intro: steps_plusI fin_steps_plusI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done