# HG changeset patch
# User haftmann
# Date 1204054697 -3600
# Node ID cf2cccf17d6d346fbb4a9b1498f2f7427d55dfa6
# Parent  4a9b8f15ce7f8e555c9f7b572fc3254e03bcc3c9
some more primrec

diff -r 4a9b8f15ce7f -r cf2cccf17d6d src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Tue Feb 26 20:38:16 2008 +0100
+++ b/src/HOL/Library/AssocList.thy	Tue Feb 26 20:38:17 2008 +0100
@@ -16,29 +16,27 @@
   to establish the invariant, e.g. for inductive proofs.
 *}
 
-fun
+primrec
   delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
     "delete k [] = []"
   | "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
 
-fun
+primrec
   update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
     "update k v [] = [(k, v)]"
   | "update k v (p#ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
 
-function
+primrec
   updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
     "updates [] vs ps = ps"
   | "updates (k#ks) vs ps = (case vs
       of [] \<Rightarrow> ps
        | (v#vs') \<Rightarrow> updates ks vs' (update k v ps))"
-by pat_completeness auto
-termination by lexicographic_order
 
-fun
+primrec
   merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
     "merge qs [] = qs"
@@ -66,23 +64,21 @@
   finally show ?thesis .
 qed
 
-function
+fun
   compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
 where
     "compose [] ys = []"
   | "compose (x#xs) ys = (case map_of ys (snd x)
        of None \<Rightarrow> compose (delete (fst x) xs) ys
         | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
-by pat_completeness auto
-termination by lexicographic_order
 
-fun
+primrec
   restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
     "restrict A [] = []"
   | "restrict A (p#ps) = (if fst p \<in> A then p#restrict A ps else restrict A ps)"
 
-fun
+primrec
   map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
     "map_ran f [] = []"
diff -r 4a9b8f15ce7f -r cf2cccf17d6d src/HOL/Library/Char_nat.thy
--- a/src/HOL/Library/Char_nat.thy	Tue Feb 26 20:38:16 2008 +0100
+++ b/src/HOL/Library/Char_nat.thy	Tue Feb 26 20:38:17 2008 +0100
@@ -11,7 +11,7 @@
 
 text {* Conversions between nibbles and natural numbers in [0..15]. *}
 
-fun
+primrec
   nat_of_nibble :: "nibble \<Rightarrow> nat" where
     "nat_of_nibble Nibble0 = 0"
   | "nat_of_nibble Nibble1 = 1"
@@ -119,7 +119,7 @@
   "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat n)"
   unfolding nibble_of_nat_norm [of n, symmetric] nibble_pair_of_nat_def ..
 
-fun
+primrec
   nat_of_char :: "char \<Rightarrow> nat" where
   "nat_of_char (Char n m) = nat_of_nibble n * 16 + nat_of_nibble m"