equal
deleted
inserted
replaced
13 |
13 |
14 axioms |
14 axioms |
15 NbT_pos: "0 < NbT" |
15 NbT_pos: "0 < NbT" |
16 |
16 |
17 (*This function merely sums the elements of a list*) |
17 (*This function merely sums the elements of a list*) |
18 consts tokens :: "nat list => nat" |
18 primrec tokens :: "nat list => nat" where |
19 primrec |
|
20 "tokens [] = 0" |
19 "tokens [] = 0" |
21 "tokens (x#xs) = x + tokens xs" |
20 | "tokens (x#xs) = x + tokens xs" |
22 |
21 |
23 consts |
22 abbreviation (input) "bag_of \<equiv> multiset_of" |
24 bag_of :: "'a list => 'a multiset" |
|
25 |
|
26 primrec |
|
27 "bag_of [] = {#}" |
|
28 "bag_of (x#xs) = {#x#} + bag_of xs" |
|
29 |
23 |
30 lemma setsum_fun_mono [rule_format]: |
24 lemma setsum_fun_mono [rule_format]: |
31 "!!f :: nat=>nat. |
25 "!!f :: nat=>nat. |
32 (ALL i. i<n --> f i <= g i) --> |
26 (ALL i. i<n --> f i <= g i) --> |
33 setsum f (lessThan n) <= setsum g (lessThan n)" |
27 setsum f (lessThan n) <= setsum g (lessThan n)" |