src/HOL/List.thy
changeset 24286 7619080e49f0
parent 24219 e558fe311376
child 24308 700e745994c1
     1.1 --- a/src/HOL/List.thy	Wed Aug 15 09:02:11 2007 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Aug 15 12:52:56 2007 +0200
     1.3 @@ -436,7 +436,7 @@
     1.4  lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
     1.5  by (induct xs) auto
     1.6  
     1.7 -lemma append_eq_append_conv [simp]:
     1.8 +lemma append_eq_append_conv [simp,noatp]:
     1.9   "!!ys. length xs = length ys \<or> length us = length vs
    1.10   ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
    1.11  apply (induct xs)
    1.12 @@ -469,7 +469,7 @@
    1.13  lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
    1.14  using append_same_eq [of "[]"] by auto
    1.15  
    1.16 -lemma hd_Cons_tl [simp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
    1.17 +lemma hd_Cons_tl [simp,noatp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
    1.18  by (induct xs) auto
    1.19  
    1.20  lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
    1.21 @@ -2391,10 +2391,10 @@
    1.22    for A :: "'a set"
    1.23  where
    1.24      Nil [intro!]: "[]: lists A"
    1.25 -  | Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A"
    1.26 -
    1.27 -inductive_cases listsE [elim!]: "x#l : lists A"
    1.28 -inductive_cases listspE [elim!]: "listsp A (x # l)"
    1.29 +  | Cons [intro!,noatp]: "[| a: A;l: lists A|] ==> a#l : lists A"
    1.30 +
    1.31 +inductive_cases listsE [elim!,noatp]: "x#l : lists A"
    1.32 +inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
    1.33  
    1.34  lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
    1.35    by (clarify, erule listsp.induct, blast+)
    1.36 @@ -2429,15 +2429,15 @@
    1.37  
    1.38  lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
    1.39  
    1.40 -lemma in_listspD [dest!]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
    1.41 +lemma in_listspD [dest!,noatp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
    1.42  by (rule in_listsp_conv_set [THEN iffD1])
    1.43  
    1.44 -lemmas in_listsD [dest!] = in_listspD [to_set]
    1.45 -
    1.46 -lemma in_listspI [intro!]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
    1.47 +lemmas in_listsD [dest!,noatp] = in_listspD [to_set]
    1.48 +
    1.49 +lemma in_listspI [intro!,noatp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
    1.50  by (rule in_listsp_conv_set [THEN iffD2])
    1.51  
    1.52 -lemmas in_listsI [intro!] = in_listspI [to_set]
    1.53 +lemmas in_listsI [intro!,noatp] = in_listspI [to_set]
    1.54  
    1.55  lemma lists_UNIV [simp]: "lists UNIV = UNIV"
    1.56  by auto