diff -r 77d5181490ae -r d131cd45a346 thys/LexerExt.thy
--- a/thys/LexerExt.thy	Tue Feb 28 23:40:37 2017 +0000
+++ b/thys/LexerExt.thy	Wed Mar 01 00:13:15 2017 +0000
@@ -84,11 +84,6 @@
   shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)"
 by(induct n) (auto simp add: Sequ_def)
 
-lemma Pow_plus:
-  "A \<up> (n + m) = A \<up> n ;; A \<up> m"
-by (induct n) (simp_all add: seq_assoc)
-
-
 section {* Kleene Star for Languages *}
 
 inductive_set
@@ -223,9 +218,6 @@
 apply(auto simp add: Sequ_def) 
 done
 
-lemma Suc_reduce_Union:
-  "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))"
-by (metis UN_extend_simps(10) image_Suc_atLeastAtMost)
 
 lemma Suc_reduce_Union2:
   "(\<Union>x\<in>{Suc n..}. B x) = (\<Union>x\<in>{n..}. B (Suc x))"
@@ -239,10 +231,6 @@
   shows "(\<Union>x\<in>A. B ;; C x) = B ;; (\<Union>x\<in>A. C x)"
 by (auto simp add: Sequ_def)
 
-lemma Seq_Union:
-  shows "A ;; (\<Union>x\<in>B. C x) = (\<Union>x\<in>B. A ;; C x)"
-by (auto simp add: Sequ_def)
-
 lemma Der_Pow [simp]:
   shows "Der c (A \<up> (Suc n)) = 
      (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})"
@@ -281,14 +269,7 @@
 apply(simp)
 by (smt Der_Pow Suc_Union inf_sup_aci(5) inf_sup_aci(7) sup_idem)
 
-lemma Der_Pow_in:
-  assumes "[] \<in> A"
-  shows "Der c (A \<up> n) = (\<Union>x\<le>n. Der c (A \<up> x))"
-using assms 
-apply(induct n)
-apply(simp)
-apply(simp add: Suc_Union)
-done
+
 
 lemma Der_Pow_notin:
   assumes "[] \<notin> A"
@@ -1277,5 +1258,5 @@
 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce
 using Posix1(1) lexer_correct_None lexer_correct_Some by blast
 
-
+unused_thms
 end
\ No newline at end of file