# HG changeset patch
# User haftmann
# Date 1180964611 -7200
# Node ID eb365b39b36d8a94d0fc221f5d504f12080b3fca
# Parent  b78bce9a0bcc96ffa892eaf663327e6dbc11ba7e
authentic syntax for List.append

diff -r b78bce9a0bcc -r eb365b39b36d src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Mon Jun 04 15:43:30 2007 +0200
+++ b/src/HOL/Induct/SList.thy	Mon Jun 04 15:43:31 2007 +0200
@@ -24,7 +24,9 @@
 Tidied by lcp.  Still needs removal of nat_rec.
 *)
 
-theory SList imports Sexp begin
+theory SList
+imports Sexp
+begin
 
 (*Hilbert_Choice is needed for the function "inv"*)
 
@@ -77,12 +79,12 @@
 
 (*Declaring the abstract list constructors*)
 
-no_translations
+(*<*)no_translations
   "[x, xs]" == "x#[xs]"
   "[x]" == "x#[]"
 no_syntax
   Nil :: "'a list"  ("[]")
-  Cons :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixr "#" 65)
+  Cons :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixr "#" 65)(*>*)
 
 definition
   Nil       :: "'a list"                               ("[]") where
@@ -159,10 +161,8 @@
   map       :: "('a=>'b) => ('a list => 'b list)" where
   "map f xs = list_rec xs [] (%x l r. f(x)#r)"
 
-no_syntax
-  append :: "'a list => 'a list => 'a list" (infixr "@" 65)
-hide const "List.append"
-
+(*<*)no_syntax
+  "\<^const>List.append" :: "'a list => 'a list => 'a list" (infixr "@" 65)(*>*)
 definition
   append    :: "['a list, 'a list] => 'a list"   (infixr "@" 65) where
   "xs@ys = list_rec xs ys (%x l r. x#r)"
@@ -230,8 +230,6 @@
   enum_Suc: "enum i (Suc j) = (if i <= j then enum i j @ [j] else [])"
 
 
-no_syntax
-  "@" :: "'a list => 'a list => 'a list"    (infixr 65)
 no_translations
   "[x:xs . P]" == "filter (%x. P) xs"
 
diff -r b78bce9a0bcc -r eb365b39b36d src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Jun 04 15:43:30 2007 +0200
+++ b/src/HOL/List.thy	Mon Jun 04 15:43:31 2007 +0200
@@ -17,7 +17,6 @@
 subsection{*Basic list processing functions*}
 
 consts
-  append :: "'a list => 'a list => 'a list" (infixr "@" 65)
   filter:: "('a => bool) => 'a list => 'a list"
   concat:: "'a list list => 'a list"
   foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
@@ -110,9 +109,14 @@
   "map f [] = []"
   "map f (x#xs) = f(x)#map f xs"
 
-primrec
-  append_Nil: "[]@ys = ys"
-  append_Cons: "(x#xs)@ys = x#(xs@ys)"
+function (*authentic syntax for append -- revert to primrec
+  as soon as "authentic" primrec is available*)
+  append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
+where
+  append_Nil: "[] @ ys = ys"
+  | append_Cons: "(x # xs) @ ys = x # (xs @ ys)"
+by (auto, case_tac a, auto)
+termination by (relation "measure (size o fst)") auto
 
 primrec
   "rev([]) = []"