src/HOL/Word/Bool_List_Representation.thy
changeset 46655 be76913ec1a4
parent 46653 a557db8f2fbf
child 47108 2a1953f0d20d
equal deleted inserted replaced
46654:134b74908a8e 46655:be76913ec1a4
   788   apply clarsimp
   788   apply clarsimp
   789   apply (case_tac bina rule: bin_exhaust)
   789   apply (case_tac bina rule: bin_exhaust)
   790   apply (case_tac binb rule: bin_exhaust)
   790   apply (case_tac binb rule: bin_exhaust)
   791   apply (case_tac b)
   791   apply (case_tac b)
   792    apply (case_tac [!] "ba")
   792    apply (case_tac [!] "ba")
   793      apply (auto simp: rbl_succ succ_def bin_to_bl_aux_alt Let_def add_ac)
   793      apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def add_ac)
   794   done
   794   done
   795 
   795 
   796 lemma rbl_add_app2: 
   796 lemma rbl_add_app2: 
   797   "!!blb. length blb >= length bla ==> 
   797   "!!blb. length blb >= length bla ==> 
   798     rbl_add bla (blb @ blc) = rbl_add bla blb"
   798     rbl_add bla (blb @ blc) = rbl_add bla blb"