equal
deleted
inserted
replaced
25 last:: "'a list => 'a" |
25 last:: "'a list => 'a" |
26 butlast :: "'a list => 'a list" |
26 butlast :: "'a list => 'a list" |
27 set :: "'a list => 'a set" |
27 set :: "'a list => 'a set" |
28 map :: "('a=>'b) => ('a list => 'b list)" |
28 map :: "('a=>'b) => ('a list => 'b list)" |
29 listsum :: "'a list => 'a::monoid_add" |
29 listsum :: "'a list => 'a::monoid_add" |
30 nth :: "'a list => nat => 'a" (infixl "!" 100) |
|
31 list_update :: "'a list => nat => 'a => 'a list" |
30 list_update :: "'a list => nat => 'a => 'a list" |
32 take:: "nat => 'a list => 'a list" |
31 take:: "nat => 'a list => 'a list" |
33 drop:: "nat => 'a list => 'a list" |
32 drop:: "nat => 'a list => 'a list" |
34 takeWhile :: "('a => bool) => 'a list => 'a list" |
33 takeWhile :: "('a => bool) => 'a list => 'a list" |
35 dropWhile :: "('a => bool) => 'a list => 'a list" |
34 dropWhile :: "('a => bool) => 'a list => 'a list" |
144 take_Nil:"take n [] = []" |
143 take_Nil:"take n [] = []" |
145 take_Cons: "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)" |
144 take_Cons: "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)" |
146 -- {*Warning: simpset does not contain this definition, but separate |
145 -- {*Warning: simpset does not contain this definition, but separate |
147 theorems for @{text "n = 0"} and @{text "n = Suc k"} *} |
146 theorems for @{text "n = 0"} and @{text "n = Suc k"} *} |
148 |
147 |
149 primrec |
148 primrec nth :: "'a list => nat => 'a" (infixl "!" 100) where |
150 nth_Cons:"(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)" |
149 nth_Cons: "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)" |
151 -- {*Warning: simpset does not contain this definition, but separate |
150 -- {*Warning: simpset does not contain this definition, but separate |
152 theorems for @{text "n = 0"} and @{text "n = Suc k"} *} |
151 theorems for @{text "n = 0"} and @{text "n = Suc k"} *} |
153 |
152 |
154 primrec |
153 primrec |
155 "[][i:=v] = []" |
154 "[][i:=v] = []" |