# HG changeset patch
# User blanchet
# Date 1392190556 -3600
# Node ID 0a155051bd9dcd0f398d798a80fac9bb082a3932
# Parent  5cb95b79a51f6bc7609bd9b23a9cd8ae9ac029a3
use new selector support to define 'the', 'hd', 'tl'

diff -r 5cb95b79a51f -r 0a155051bd9d src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/List.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -9,8 +9,8 @@
 begin
 
 datatype_new 'a list =
-    Nil    ("[]")
-  | Cons 'a  "'a list"    (infixr "#" 65)
+    =: Nil (defaults tl: "[]")  ("[]")
+  | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)
 
 datatype_new_compat list
 
@@ -34,13 +34,6 @@
 
 subsection {* Basic list processing functions *}
 
-primrec hd :: "'a list \<Rightarrow> 'a" where
-"hd (x # xs) = x"
-
-primrec tl :: "'a list \<Rightarrow> 'a list" where
-"tl [] = []" |
-"tl (x # xs) = xs"
-
 primrec last :: "'a list \<Rightarrow> 'a" where
 "last (x # xs) = (if xs = [] then x else last xs)"
 
@@ -3390,7 +3383,8 @@
 
 lemma distinct_length_2_or_more:
 "distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
-by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons)
+by (metis distinct.simps(2) list.sel(1) hd_in_set list.simps(2) set_ConsD set_rev_mp
+      set_subset_Cons)
 
 lemma remdups_adj_Cons: "remdups_adj (x # xs) =
   (case remdups_adj xs of [] \<Rightarrow> [x] | y # xs \<Rightarrow> if x = y then y # xs else x # y # xs)"
@@ -6695,7 +6689,7 @@
 
 lemma tl_transfer [transfer_rule]:
   "(list_all2 A ===> list_all2 A) tl tl"
-  unfolding tl_def by transfer_prover
+  unfolding tl_def[abs_def] by transfer_prover
 
 lemma butlast_transfer [transfer_rule]:
   "(list_all2 A ===> list_all2 A) butlast butlast"
diff -r 5cb95b79a51f -r 0a155051bd9d src/HOL/Option.thy
--- a/src/HOL/Option.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Option.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -8,7 +8,7 @@
 imports BNF_LFP Datatype Finite_Set
 begin
 
-datatype_new 'a option = None | Some 'a
+datatype_new 'a option = =: None | Some (the: 'a)
 
 datatype_new_compat option
 
@@ -52,9 +52,6 @@
 
 subsubsection {* Operations *}
 
-primrec the :: "'a option => 'a" where
-"the (Some x) = x"
-
 primrec set :: "'a option => 'a set" where
 "set None = {}" |
 "set (Some x) = {x}"