src/HOL/List.thy
changeset 55405 0a155051bd9d
parent 55404 5cb95b79a51f
child 55406 186076d100d3
     1.1 --- a/src/HOL/List.thy	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -9,8 +9,8 @@
     1.4  begin
     1.5  
     1.6  datatype_new 'a list =
     1.7 -    Nil    ("[]")
     1.8 -  | Cons 'a  "'a list"    (infixr "#" 65)
     1.9 +    =: Nil (defaults tl: "[]")  ("[]")
    1.10 +  | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)
    1.11  
    1.12  datatype_new_compat list
    1.13  
    1.14 @@ -34,13 +34,6 @@
    1.15  
    1.16  subsection {* Basic list processing functions *}
    1.17  
    1.18 -primrec hd :: "'a list \<Rightarrow> 'a" where
    1.19 -"hd (x # xs) = x"
    1.20 -
    1.21 -primrec tl :: "'a list \<Rightarrow> 'a list" where
    1.22 -"tl [] = []" |
    1.23 -"tl (x # xs) = xs"
    1.24 -
    1.25  primrec last :: "'a list \<Rightarrow> 'a" where
    1.26  "last (x # xs) = (if xs = [] then x else last xs)"
    1.27  
    1.28 @@ -3390,7 +3383,8 @@
    1.29  
    1.30  lemma distinct_length_2_or_more:
    1.31  "distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
    1.32 -by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons)
    1.33 +by (metis distinct.simps(2) list.sel(1) hd_in_set list.simps(2) set_ConsD set_rev_mp
    1.34 +      set_subset_Cons)
    1.35  
    1.36  lemma remdups_adj_Cons: "remdups_adj (x # xs) =
    1.37    (case remdups_adj xs of [] \<Rightarrow> [x] | y # xs \<Rightarrow> if x = y then y # xs else x # y # xs)"
    1.38 @@ -6695,7 +6689,7 @@
    1.39  
    1.40  lemma tl_transfer [transfer_rule]:
    1.41    "(list_all2 A ===> list_all2 A) tl tl"
    1.42 -  unfolding tl_def by transfer_prover
    1.43 +  unfolding tl_def[abs_def] by transfer_prover
    1.44  
    1.45  lemma butlast_transfer [transfer_rule]:
    1.46    "(list_all2 A ===> list_all2 A) butlast butlast"