summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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 {} = {[]}" |