summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/List.thy

changeset 53689 | 705f0b728b1b |

parent 53412 | 01b804df0a30 |

child 53721 | ccaceea6c768 |

1.1 --- a/src/HOL/List.thy Wed Sep 18 00:11:15 2013 +0200 1.2 +++ b/src/HOL/List.thy Wed Sep 18 12:16:10 2013 +0200 1.3 @@ -710,9 +710,15 @@ 1.4 lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)" 1.5 by (induct xs) auto 1.6 1.7 +lemma tl_Nil: "tl xs = [] \<longleftrightarrow> xs = [] \<or> (EX x. xs = [x])" 1.8 +by (cases xs) auto 1.9 + 1.10 +lemma Nil_tl: "[] = tl xs \<longleftrightarrow> xs = [] \<or> (EX x. xs = [x])" 1.11 +by (cases xs) auto 1.12 + 1.13 lemma length_induct: 1.14 "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs" 1.15 -by (rule measure_induct [of length]) iprover 1.16 +by (fact measure_induct) 1.17 1.18 lemma list_nonempty_induct [consumes 1, case_names single cons]: 1.19 assumes "xs \<noteq> []"