src/HOL/List.thy
 changeset 46440 d4994e2e7364 parent 46439 2388be11cb50 child 46448 f1201fac7398
equal inserted replaced
46439:2388be11cb50 46440:d4994e2e7364
   204
   204
   205 abbreviation
   205 abbreviation
   206   length :: "'a list \<Rightarrow> nat" where
   206   length :: "'a list \<Rightarrow> nat" where
   207   "length \<equiv> size"
   207   "length \<equiv> size"
   208
   208
   209 definition
   209 primrec rotate1 :: "'a list \<Rightarrow> 'a list" where
   210   rotate1 :: "'a list \<Rightarrow> 'a list" where
   210   "rotate1 [] = []" |
   211   "rotate1 xs = (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])"
   211   "rotate1 (x # xs) = xs @ [x]"
   212
   212
   213 definition
   213 definition
   214   rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   214   rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   215   "rotate n = rotate1 ^^ n"
   215   "rotate n = rotate1 ^^ n"
   216
   216
   263 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
   263 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
   264 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
   264 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
   265 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
   265 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
   266 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
   266 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
   267 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
   267 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
   268 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\
   268 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\
   269 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def eval_nat_numeral)}\\
   269 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
   270 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
   270 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
   271 @{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\
   271 @{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\
   272 @{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def foldr_def)}
   272 @{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def foldr_def)}
   273 \end{tabular}}
   273 \end{tabular}}
   274 \caption{Characteristic examples}
   274 \caption{Characteristic examples}
  2878
  2878
  2879 lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
  2879 lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
  2880 by (metis distinct_remdups finite_list set_remdups)
  2880 by (metis distinct_remdups finite_list set_remdups)
  2881
  2881
  2882 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
  2882 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
  2883 by (induct x, auto)
  2883 by (induct x, auto)
  2884
  2884
  2885 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
  2885 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
  2886 by (induct x, auto)
  2886 by (induct x, auto)
  2887
  2887
  2888 lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
  2888 lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
  2965 apply (rule iffI, clarsimp)
  2965 apply (rule iffI, clarsimp)
  2966  apply (case_tac i)
  2966  apply (case_tac i)
  2967 apply (case_tac j, simp)
  2967 apply (case_tac j, simp)
  2968 apply (simp add: set_conv_nth)
  2968 apply (simp add: set_conv_nth)
  2969  apply (case_tac j)
  2969  apply (case_tac j)
  2970 apply (clarsimp simp add: set_conv_nth, simp)
  2970 apply (clarsimp simp add: set_conv_nth, simp)
  2971 apply (rule conjI)
  2971 apply (rule conjI)
  2972 (*TOO SLOW
  2972 (*TOO SLOW
  2973 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
  2973 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
  2974 *)
  2974 *)
  2975  apply (clarsimp simp add: set_conv_nth)
  2975  apply (clarsimp simp add: set_conv_nth)
  2997   show ?case
  2997   show ?case
  2998   proof (cases "x \<in> set xs")
  2998   proof (cases "x \<in> set xs")
  2999     case False with Cons show ?thesis by simp
  2999     case False with Cons show ?thesis by simp
  3000   next
  3000   next
  3001     case True with Cons.prems
  3001     case True with Cons.prems
  3002     have "card (set xs) = Suc (length xs)"
  3002     have "card (set xs) = Suc (length xs)"
  3003       by (simp add: card_insert_if split: split_if_asm)
  3003       by (simp add: card_insert_if split: split_if_asm)
  3004     moreover have "card (set xs) \<le> length xs" by (rule card_length)
  3004     moreover have "card (set xs) \<le> length xs" by (rule card_length)
  3005     ultimately have False by simp
  3005     ultimately have False by simp
  3006     thus ?thesis ..
  3006     thus ?thesis ..
  3007   qed
  3007   qed
  3588 qed
  3588 qed
  3589
  3589
  3590
  3590
  3591 subsubsection{*@{text rotate1} and @{text rotate}*}
  3591 subsubsection{*@{text rotate1} and @{text rotate}*}
  3592
  3592
  3596 lemma rotate0[simp]: "rotate 0 = id"
  3593 lemma rotate0[simp]: "rotate 0 = id"
  3597 by(simp add:rotate_def)
  3594 by(simp add:rotate_def)
  3598
  3595
  3599 lemma rotate_Suc[simp]: "rotate (Suc n) xs = rotate1(rotate n xs)"
  3596 lemma rotate_Suc[simp]: "rotate (Suc n) xs = rotate1(rotate n xs)"
  3600 by(simp add:rotate_def)
  3597 by(simp add:rotate_def)
  3617  apply simp
  3614  apply simp
  3618 apply (simp add:rotate_def)
  3615 apply (simp add:rotate_def)
  3619 done
  3616 done
  3620
  3617
  3621 lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
  3618 lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
  3622 by(simp add:rotate1_def split:list.split)
  3619 by (cases xs) simp_all
  3623
  3620
  3624 lemma rotate_drop_take:
  3621 lemma rotate_drop_take:
  3625   "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
  3622   "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
  3626 apply(induct n)
  3623 apply(induct n)
  3627  apply simp
  3624  apply simp
  3640
  3637
  3641 lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"
  3638 lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"
  3642 by(simp add:rotate_drop_take)
  3639 by(simp add:rotate_drop_take)
  3643
  3640
  3644 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
  3641 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
  3645 by(simp add:rotate1_def split:list.split)
  3642 by (cases xs) simp_all
  3646
  3643
  3647 lemma length_rotate[simp]: "length(rotate n xs) = length xs"
  3644 lemma length_rotate[simp]: "length(rotate n xs) = length xs"
  3648 by (induct n arbitrary: xs) (simp_all add:rotate_def)
  3645 by (induct n arbitrary: xs) (simp_all add:rotate_def)
  3649
  3646
  3650 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
  3647 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
  3651 by(simp add:rotate1_def split:list.split) blast
  3648 by (cases xs) auto
  3652
  3649
  3653 lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
  3650 lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
  3654 by (induct n) (simp_all add:rotate_def)
  3651 by (induct n) (simp_all add:rotate_def)
  3655
  3652
  3656 lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"
  3653 lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"
  3657 by(simp add:rotate_drop_take take_map drop_map)
  3654 by(simp add:rotate_drop_take take_map drop_map)
  3658
  3655
  3659 lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
  3656 lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
  3660 by (cases xs) (auto simp add:rotate1_def)
  3657 by (cases xs) auto
  3661
  3658
  3662 lemma set_rotate[simp]: "set(rotate n xs) = set xs"
  3659 lemma set_rotate[simp]: "set(rotate n xs) = set xs"
  3663 by (induct n) (simp_all add:rotate_def)
  3660 by (induct n) (simp_all add:rotate_def)
  3664
  3661
  3665 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
  3662 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
  3666 by(simp add:rotate1_def split:list.split)
  3663 by (cases xs) auto
  3667
  3664
  3668 lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
  3665 lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
  3669 by (induct n) (simp_all add:rotate_def)
  3666 by (induct n) (simp_all add:rotate_def)
  3670
  3667
  3671 lemma rotate_rev:
  3668 lemma rotate_rev: