src/HOL/Word/Bool_List_Representation.thy
changeset 45475 b2b087c20e45
parent 44939 5930d35c976d
child 45543 827bf668c822
equal deleted inserted replaced
45466:98af01f897c9 45475:b2b087c20e45
   274   apply (cut_tac x=n and y="size list" in linorder_less_linear)
   274   apply (cut_tac x=n and y="size list" in linorder_less_linear)
   275   apply (erule disjE, simp add: nth_append)+
   275   apply (erule disjE, simp add: nth_append)+
   276   apply auto
   276   apply auto
   277   done
   277   done
   278 
   278 
   279 lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)";
   279 lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)"
   280   unfolding bl_to_bin_def by (simp add : bin_nth_of_bl_aux)
   280   unfolding bl_to_bin_def by (simp add : bin_nth_of_bl_aux)
   281 
   281 
   282 lemma bin_nth_bl [rule_format] : "ALL m w. n < m --> 
   282 lemma bin_nth_bl [rule_format] : "ALL m w. n < m --> 
   283     bin_nth w n = nth (rev (bin_to_bl m w)) n"
   283     bin_nth w n = nth (rev (bin_to_bl m w)) n"
   284   apply (induct n)
   284   apply (induct n)
   715 lemma bl_of_nth_inj: 
   715 lemma bl_of_nth_inj: 
   716   "(!!k. k < n ==> f k = g k) ==> bl_of_nth n f = bl_of_nth n g"
   716   "(!!k. k < n ==> f k = g k) ==> bl_of_nth n f = bl_of_nth n g"
   717   by (induct n)  auto
   717   by (induct n)  auto
   718 
   718 
   719 lemma bl_of_nth_nth_le [rule_format] : "ALL xs. 
   719 lemma bl_of_nth_nth_le [rule_format] : "ALL xs. 
   720     length xs >= n --> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs";
   720     length xs >= n --> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
   721   apply (induct n, clarsimp)
   721   apply (induct n, clarsimp)
   722   apply clarsimp
   722   apply clarsimp
   723   apply (rule trans [OF _ hd_Cons_tl])
   723   apply (rule trans [OF _ hd_Cons_tl])
   724    apply (frule Suc_le_lessD)
   724    apply (frule Suc_le_lessD)
   725    apply (simp add: nth_rev trans [OF drop_Suc drop_tl, symmetric])
   725    apply (simp add: nth_rev trans [OF drop_Suc drop_tl, symmetric])