--- a/thys/Simplifying.thy	Wed Mar 16 10:02:19 2016 +0000
+++ b/thys/Simplifying.thy	Fri Mar 18 01:26:14 2016 +0000
@@ -37,74 +37,17 @@
 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)"
 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)"  
  
-lemma simp_SEQ_simps:
+lemma simp_SEQ_simps[simp]:
   "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2))
                     else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2))
                     else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))"
-apply(auto)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac a)
-apply(simp_all)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac a)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(auto)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-done
+by (induct p1 p2 rule: simp_SEQ.induct) (auto)
 
-lemma simp_ALT_simps:
+lemma simp_ALT_simps[simp]:
   "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2))
                     else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1))
                     else (ALT (fst p1) (fst p2), F_ALT (snd p1) (snd p2))))"
-apply(auto)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac a)
-apply(simp_all)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac a)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(auto)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-done
-
+by (induct p1 p2 rule: simp_ALT.induct) (auto)
 
 fun 
   simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)"
@@ -126,15 +69,14 @@
 lemma L_fst_simp:
   shows "L(r) = L(fst (simp r))"
 using assms
-apply(induct r rule: rexp.induct)
-apply(auto simp add: simp_SEQ_simps simp_ALT_simps)
-done
+by (induct r) (auto)
+
 
 lemma 
   shows "\<turnstile> ((snd (simp r)) v) : r \<longleftrightarrow> \<turnstile> v : (fst (simp r))"
 using assms
 apply(induct r arbitrary: v rule: simp.induct)
-apply(auto simp add: simp_SEQ_simps simp_ALT_simps intro: Prf.intros)
+apply(auto intro: Prf.intros)
 using Prf_elims(3) apply blast
 apply(erule Prf_elims)
 apply(simp)
@@ -210,7 +152,7 @@
   shows "((snd (simp r)) v) = mkeps r"
 using assms 
 apply(induct r arbitrary: v)
-apply(auto simp add: simp_SEQ_simps simp_ALT_simps)
+apply(auto)
 apply(erule Posix_elims)
 apply(simp)
 apply(erule Posix_elims)
@@ -254,7 +196,7 @@
   shows "s \<in> r \<rightarrow> ((snd (simp r)) v)"
 using assms
 apply(induct r arbitrary: s v rule: rexp.induct) 
-apply(auto split: if_splits simp add: simp_SEQ_simps simp_ALT_simps)
+apply(auto split: if_splits)
 prefer 3
 apply(erule Posix_elims)
 apply(clarify)
@@ -311,7 +253,6 @@
   shows "slexer r s = lexer r s"
 apply(induct s arbitrary: r)
 apply(simp)
-apply(simp)
 apply(auto split: option.split prod.split)
 apply (metis L_fst_simp fst_conv lexer_correct_None)
 using L_fst_simp lexer_correct_None apply fastforce