src/HOL/List.thy
changeset 54147 97a8ff4e4ac9
parent 53954 ccfd22f937be
child 54295 45a5523d4a63
equal deleted inserted replaced
54146:97f69d44f732 54147:97a8ff4e4ac9
   900 by (induct xs) auto
   900 by (induct xs) auto
   901 
   901 
   902 lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
   902 lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
   903 by (induct xs) auto
   903 by (induct xs) auto
   904 
   904 
   905 lemma append_eq_append_conv [simp, no_atp]:
   905 lemma append_eq_append_conv [simp]:
   906  "length xs = length ys \<or> length us = length vs
   906  "length xs = length ys \<or> length us = length vs
   907  ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
   907  ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
   908 apply (induct xs arbitrary: ys)
   908 apply (induct xs arbitrary: ys)
   909  apply (case_tac ys, simp, force)
   909  apply (case_tac ys, simp, force)
   910 apply (case_tac ys, force, simp)
   910 apply (case_tac ys, force, simp)
   932 using append_same_eq [of _ _ "[]"] by auto
   932 using append_same_eq [of _ _ "[]"] by auto
   933 
   933 
   934 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
   934 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
   935 using append_same_eq [of "[]"] by auto
   935 using append_same_eq [of "[]"] by auto
   936 
   936 
   937 lemma hd_Cons_tl [simp,no_atp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
   937 lemma hd_Cons_tl [simp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
   938 by (induct xs) auto
   938 by (induct xs) auto
   939 
   939 
   940 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
   940 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
   941 by (induct xs) auto
   941 by (induct xs) auto
   942 
   942 
  1176 by (cases xs) auto
  1176 by (cases xs) auto
  1177 
  1177 
  1178 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
  1178 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
  1179 by (cases xs) auto
  1179 by (cases xs) auto
  1180 
  1180 
  1181 lemma rev_is_rev_conv [iff, no_atp]: "(rev xs = rev ys) = (xs = ys)"
  1181 lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
  1182 apply (induct xs arbitrary: ys, force)
  1182 apply (induct xs arbitrary: ys, force)
  1183 apply (case_tac ys, simp, force)
  1183 apply (case_tac ys, simp, force)
  1184 done
  1184 done
  1185 
  1185 
  1186 lemma inj_on_rev[iff]: "inj_on rev A"
  1186 lemma inj_on_rev[iff]: "inj_on rev A"
  5082 inductive_set
  5082 inductive_set
  5083   lists :: "'a set => 'a list set"
  5083   lists :: "'a set => 'a list set"
  5084   for A :: "'a set"
  5084   for A :: "'a set"
  5085 where
  5085 where
  5086     Nil [intro!, simp]: "[]: lists A"
  5086     Nil [intro!, simp]: "[]: lists A"
  5087   | Cons [intro!, simp, no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
  5087   | Cons [intro!, simp]: "[| a: A; l: lists A|] ==> a#l : lists A"
  5088 
  5088 
  5089 inductive_cases listsE [elim!,no_atp]: "x#l : lists A"
  5089 inductive_cases listsE [elim!]: "x#l : lists A"
  5090 inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"
  5090 inductive_cases listspE [elim!]: "listsp A (x # l)"
  5091 
  5091 
  5092 inductive_simps listsp_simps[code]:
  5092 inductive_simps listsp_simps[code]:
  5093   "listsp A []"
  5093   "listsp A []"
  5094   "listsp A (x # xs)"
  5094   "listsp A (x # xs)"
  5095 
  5095 
  5127 -- {* eliminate @{text listsp} in favour of @{text set} *}
  5127 -- {* eliminate @{text listsp} in favour of @{text set} *}
  5128 by (induct xs) auto
  5128 by (induct xs) auto
  5129 
  5129 
  5130 lemmas in_lists_conv_set [code_unfold] = in_listsp_conv_set [to_set]
  5130 lemmas in_lists_conv_set [code_unfold] = in_listsp_conv_set [to_set]
  5131 
  5131 
  5132 lemma in_listspD [dest!,no_atp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
  5132 lemma in_listspD [dest!]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
  5133 by (rule in_listsp_conv_set [THEN iffD1])
  5133 by (rule in_listsp_conv_set [THEN iffD1])
  5134 
  5134 
  5135 lemmas in_listsD [dest!,no_atp] = in_listspD [to_set]
  5135 lemmas in_listsD [dest!] = in_listspD [to_set]
  5136 
  5136 
  5137 lemma in_listspI [intro!,no_atp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
  5137 lemma in_listspI [intro!]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
  5138 by (rule in_listsp_conv_set [THEN iffD2])
  5138 by (rule in_listsp_conv_set [THEN iffD2])
  5139 
  5139 
  5140 lemmas in_listsI [intro!,no_atp] = in_listspI [to_set]
  5140 lemmas in_listsI [intro!] = in_listspI [to_set]
  5141 
  5141 
  5142 lemma lists_eq_set: "lists A = {xs. set xs <= A}"
  5142 lemma lists_eq_set: "lists A = {xs. set xs <= A}"
  5143 by auto
  5143 by auto
  5144 
  5144 
  5145 lemma lists_empty [simp]: "lists {} = {[]}"
  5145 lemma lists_empty [simp]: "lists {} = {[]}"