# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1566429067 -7200
# Node ID c7fd85daa1d7aef6cac77da88a1ef91bf875f96b
# Parent  4e73568b9cf643c53d6ecfe564e11ff1ae2305ea
updated with the proof of bder

diff -r 4e73568b9cf6 -r c7fd85daa1d7 thys/BitCoded2.thy
--- a/thys/BitCoded2.thy	Wed Aug 21 10:29:34 2019 +0200
+++ b/thys/BitCoded2.thy	Thu Aug 22 01:11:07 2019 +0200
@@ -3621,18 +3621,7 @@
   apply(subgoal_tac "rsX \<noteq> []")
    prefer 2
    apply (metis arexp.distinct(7) good.simps(4) good1)
-  apply(subgoal_tac "\<exists>XX. XX \<in> set rsX")
-   prefer 2
-  using neq_Nil_conv apply fastforce
-  apply(erule exE)
-  apply(rule_tac x="fuse bsX XX" in bexI)
-   prefer 2
-   apply blast
-  apply(frule f_cont1)
-  apply(auto)
-  apply(rule contains0)
-  apply(drule contains49)
-  by (simp add: in2)
+  by (metis contains0 contains49 f_cont1 in2 list.exhaust list.set_intros(1))
 
 lemma CONTAINS1:
   assumes "a >> bs"
@@ -3800,6 +3789,7 @@
   assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
   shows "bsimp r = XXX"
   and   "bder c r = XXX"
+  and   "bder c (bsimp r) = XXX"
   and   "bsimp (bder c (bsimp r)) = XXX"
   and   "bsimp (bder c r) = XXX"
   apply(simp_all add: assms)