src/HOL/List.thy
changeset 44890 22f665a2e91c
parent 44635 3d046864ebe6
child 44916 840d8c3d9113
equal deleted inserted replaced
44889:340df9f3491f 44890:22f665a2e91c
   657 done
   657 done
   658 
   658 
   659 lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =
   659 lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =
   660   (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"
   660   (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"
   661 apply (induct xs arbitrary: ys zs ts)
   661 apply (induct xs arbitrary: ys zs ts)
   662  apply fastsimp
   662  apply fastforce
   663 apply(case_tac zs)
   663 apply(case_tac zs)
   664  apply simp
   664  apply simp
   665 apply fastsimp
   665 apply fastforce
   666 done
   666 done
   667 
   667 
   668 lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)"
   668 lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)"
   669 by simp
   669 by simp
   670 
   670 
   995   case Nil thus ?case by simp
   995   case Nil thus ?case by simp
   996 next
   996 next
   997   case (Cons a xs)
   997   case (Cons a xs)
   998   show ?case
   998   show ?case
   999   proof cases
   999   proof cases
  1000     assume "x = a" thus ?case using Cons by fastsimp
  1000     assume "x = a" thus ?case using Cons by fastforce
  1001   next
  1001   next
  1002     assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI)
  1002     assume "x \<noteq> a" thus ?case using Cons by(fastforce intro!: Cons_eq_appendI)
  1003   qed
  1003   qed
  1004 qed
  1004 qed
  1005 
  1005 
  1006 lemma in_set_conv_decomp_first:
  1006 lemma in_set_conv_decomp_first:
  1007   "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"
  1007   "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"
  1014   case (snoc a xs)
  1014   case (snoc a xs)
  1015   show ?case
  1015   show ?case
  1016   proof cases
  1016   proof cases
  1017     assume "x = a" thus ?case using snoc by (metis List.set.simps(1) emptyE)
  1017     assume "x = a" thus ?case using snoc by (metis List.set.simps(1) emptyE)
  1018   next
  1018   next
  1019     assume "x \<noteq> a" thus ?case using snoc by fastsimp
  1019     assume "x \<noteq> a" thus ?case using snoc by fastforce
  1020   qed
  1020   qed
  1021 qed
  1021 qed
  1022 
  1022 
  1023 lemma in_set_conv_decomp_last:
  1023 lemma in_set_conv_decomp_last:
  1024   "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs)"
  1024   "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs)"
  1076   proof cases
  1076   proof cases
  1077     assume "P x" thus ?thesis by (metis emptyE set_empty)
  1077     assume "P x" thus ?thesis by (metis emptyE set_empty)
  1078   next
  1078   next
  1079     assume "\<not> P x"
  1079     assume "\<not> P x"
  1080     hence "\<exists>x\<in>set xs. P x" using snoc(2) by simp
  1080     hence "\<exists>x\<in>set xs. P x" using snoc(2) by simp
  1081     thus ?thesis using `\<not> P x` snoc(1) by fastsimp
  1081     thus ?thesis using `\<not> P x` snoc(1) by fastforce
  1082   qed
  1082   qed
  1083 qed
  1083 qed
  1084 
  1084 
  1085 lemma split_list_last_propE:
  1085 lemma split_list_last_propE:
  1086   assumes "\<exists>x \<in> set xs. P x"
  1086   assumes "\<exists>x \<in> set xs. P x"
  1214       assume "x \<noteq> y"
  1214       assume "x \<noteq> y"
  1215       with Py Cons.prems show ?thesis by simp
  1215       with Py Cons.prems show ?thesis by simp
  1216     qed
  1216     qed
  1217   next
  1217   next
  1218     assume "\<not> P y"
  1218     assume "\<not> P y"
  1219     with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastsimp
  1219     with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastforce
  1220     then have "?Q (y#us)" by simp
  1220     then have "?Q (y#us)" by simp
  1221     then show ?thesis ..
  1221     then show ?thesis ..
  1222   qed
  1222   qed
  1223 qed
  1223 qed
  1224 
  1224 
  2984 
  2984 
  2985 lemma elem_le_listsum_nat:
  2985 lemma elem_le_listsum_nat:
  2986   "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
  2986   "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
  2987 apply(induct ns arbitrary: k)
  2987 apply(induct ns arbitrary: k)
  2988  apply simp
  2988  apply simp
  2989 apply(fastsimp simp add:nth_Cons split: nat.split)
  2989 apply(fastforce simp add:nth_Cons split: nat.split)
  2990 done
  2990 done
  2991 
  2991 
  2992 lemma listsum_update_nat:
  2992 lemma listsum_update_nat:
  2993   "k<size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"
  2993   "k<size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"
  2994 apply(induct ns arbitrary:k)
  2994 apply(induct ns arbitrary:k)
  4669 lemma snoc_listrel1_snoc_iff:
  4669 lemma snoc_listrel1_snoc_iff:
  4670   "(xs @ [x], ys @ [y]) \<in> listrel1 r
  4670   "(xs @ [x], ys @ [y]) \<in> listrel1 r
  4671     \<longleftrightarrow> (xs, ys) \<in> listrel1 r \<and> x = y \<or> xs = ys \<and> (x,y) \<in> r" (is "?L \<longleftrightarrow> ?R")
  4671     \<longleftrightarrow> (xs, ys) \<in> listrel1 r \<and> x = y \<or> xs = ys \<and> (x,y) \<in> r" (is "?L \<longleftrightarrow> ?R")
  4672 proof
  4672 proof
  4673   assume ?L thus ?R
  4673   assume ?L thus ?R
  4674     by (fastsimp simp: listrel1_def snoc_eq_iff_butlast butlast_append)
  4674     by (fastforce simp: listrel1_def snoc_eq_iff_butlast butlast_append)
  4675 next
  4675 next
  4676   assume ?R then show ?L unfolding listrel1_def by force
  4676   assume ?R then show ?L unfolding listrel1_def by force
  4677 qed
  4677 qed
  4678 
  4678 
  4679 lemma listrel1_eq_len: "(xs,ys) \<in> listrel1 r \<Longrightarrow> length xs = length ys"
  4679 lemma listrel1_eq_len: "(xs,ys) \<in> listrel1 r \<Longrightarrow> length xs = length ys"
  4732 
  4732 
  4733 lemma lists_accI: "xs \<in> acc (listrel1 r) \<Longrightarrow> xs \<in> lists (acc r)"
  4733 lemma lists_accI: "xs \<in> acc (listrel1 r) \<Longrightarrow> xs \<in> lists (acc r)"
  4734 apply (induct set: acc)
  4734 apply (induct set: acc)
  4735 apply clarify
  4735 apply clarify
  4736 apply (rule accI)
  4736 apply (rule accI)
  4737 apply (fastsimp dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)
  4737 apply (fastforce dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)
  4738 done
  4738 done
  4739 
  4739 
  4740 lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r"
  4740 lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r"
  4741 by(metis wf_acc_iff in_lists_conv_set lists_accI lists_accD Cons_in_lists_iff)
  4741 by(metis wf_acc_iff in_lists_conv_set lists_accI lists_accD Cons_in_lists_iff)
  4742 
  4742