author | nipkow |

Wed Sep 18 12:16:10 2013 +0200 (2013-09-18) | |

changeset 53689 | 705f0b728b1b |

parent 53688 | 63892cfef47f |

child 53690 | a3ad5a0350f9 |

added and tuned lemmas

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> []"