# HG changeset patch
# User Chengsong
# Date 1568319174 -3600
# Node ID 744c32aceea65185bbb5f0d0414b9c8fa7669e66
# Parent  ab8977636927bc6afa0032957cf3565c4218ec2d
question

diff -r ab8977636927 -r 744c32aceea6 thys/BitCoded2CT.thy
--- a/thys/BitCoded2CT.thy	Thu Sep 12 19:44:12 2019 +0100
+++ b/thys/BitCoded2CT.thy	Thu Sep 12 21:12:54 2019 +0100
@@ -3080,7 +3080,9 @@
   apply -
   by auto
 
-
+lemma concat_def:
+  shows"[]@lst=lst"
+  
 lemma derc_alt:
   assumes "bder c (AALTs [] as) >> bs"
   shows "bder c (bsimp(AALTs [] as)) >> bs"
@@ -3092,8 +3094,13 @@
   apply(drule_tac  x="[]" in meta_spec)
   apply(drule_tac x="map (bder c) as" in meta_spec)
   apply(drule_tac x="bs" in meta_spec)
-  (*HERE*)
-  apply(drule i_know_it_must_be_a_theorem_but_dunno_its_name)
+  apply(simp add:List.append.simps(1))
+  apply(rule_tac t="as" and s="list1@[a]@list2" in subst)
+   
+(*  (*HERE*)
+  apply(drule  i_know_it_must_be_a_theorem_but_dunno_its_name)
+*)
+
   oops
 
 lemma transfer: