bag.why 3.19 KB
 Jean-Christophe Filliatre committed Apr 16, 2012 1 `````` `````` MARCHE Claude committed Apr 19, 2012 2 ``````(** {1 Multisets (aka bags)} *) `````` Jean-Christophe Filliatre committed Apr 16, 2012 3 4 5 6 7 8 9 `````` theory Bag use import int.Int type bag 'a `````` Andrei Paskevich committed Aug 03, 2013 10 11 12 `````` (** whatever ['a], the type [bag 'a] is always infinite *) meta "infinite_type" type bag `````` MARCHE Claude committed Apr 19, 2012 13 `````` (** the most basic operation is the number of occurrences *) `````` Jean-Christophe Filliatre committed Apr 16, 2012 14 15 16 17 18 19 20 `````` function nb_occ (x: 'a) (b: bag 'a): int axiom occ_non_negative: forall b: bag 'a, x: 'a. nb_occ x b >= 0 predicate mem (x: 'a) (b: bag 'a) = nb_occ x b > 0 `````` MARCHE Claude committed Apr 19, 2012 21 `````` (** equality of bags *) `````` Jean-Christophe Filliatre committed Apr 16, 2012 22 23 24 25 26 27 `````` predicate eq_bag (a b: bag 'a) = forall x:'a. nb_occ x a = nb_occ x b axiom bag_extensionality: forall a b: bag 'a. eq_bag a b -> a = b `````` MARCHE Claude committed Apr 19, 2012 28 `````` (** basic constructors of bags *) `````` Jean-Christophe Filliatre committed Apr 16, 2012 29 30 31 32 33 34 35 36 37 38 39 40 41 `````` function empty_bag: bag 'a axiom occ_empty: forall x: 'a. nb_occ x empty_bag = 0 lemma is_empty: forall b: bag 'a. (forall x: 'a. nb_occ x b = 0) -> b = empty_bag function singleton (x: 'a) : bag 'a axiom occ_singleton: forall x y: 'a. (x = y /\ (nb_occ y (singleton x)) = 1) \/ (x <> y /\ (nb_occ y (singleton x)) = 0) `````` Jean-Christophe Filliatre committed Jan 08, 2016 42 `````` (* FIXME? nb_occ y (singleton x) = if x = y then 1 else 0 *) `````` Jean-Christophe Filliatre committed Apr 16, 2012 43 44 `````` lemma occ_singleton_eq: `````` Jean-Christophe Filliatre committed Jan 08, 2016 45 `````` forall x y: 'a. x = y -> nb_occ y (singleton x) = 1 `````` Jean-Christophe Filliatre committed Apr 16, 2012 46 `````` lemma occ_singleton_neq: `````` Jean-Christophe Filliatre committed Jan 08, 2016 47 `````` forall x y: 'a. x <> y -> nb_occ y (singleton x) = 0 `````` Jean-Christophe Filliatre committed Apr 16, 2012 48 49 50 51 52 53 54 `````` function union (bag 'a) (bag 'a) : bag 'a axiom occ_union: forall x: 'a, a b: bag 'a. nb_occ x (union a b) = nb_occ x a + nb_occ x b `````` MARCHE Claude committed Apr 19, 2012 55 `````` (** union commutative, associative with identity empty_bag *) `````` Jean-Christophe Filliatre committed Apr 16, 2012 56 57 58 59 60 61 62 63 `````` lemma Union_comm: forall a b: bag 'a. union a b = union b a lemma Union_identity: forall a: bag 'a. union a empty_bag = a lemma Union_assoc: forall a b c: bag 'a. union a (union b c) = union (union a b) c `````` Jean-Christophe Filliatre committed Jan 08, 2016 64 `````` lemma bag_simpl_right: `````` Jean-Christophe Filliatre committed Apr 16, 2012 65 66 67 68 69 `````` forall a b c: bag 'a. union a b = union c b -> a = c lemma bag_simpl_left: forall a b c: bag 'a. union a b = union a c -> b = c `````` MARCHE Claude committed Apr 19, 2012 70 `````` (** add operation *) `````` Jean-Christophe Filliatre committed Apr 16, 2012 71 72 73 74 75 `````` function add (x: 'a) (b: bag 'a) : bag 'a = union (singleton x) b lemma occ_add_eq: forall b: bag 'a, x y: 'a. `````` Jean-Christophe Filliatre committed Jan 08, 2016 76 `````` x = y -> nb_occ y (add x b) = nb_occ y b + 1 `````` Jean-Christophe Filliatre committed Apr 16, 2012 77 78 79 80 `````` lemma occ_add_neq: forall b: bag 'a, x y: 'a. x <> y -> nb_occ y (add x b) = nb_occ y b `````` MARCHE Claude committed Apr 19, 2012 81 `````` (** cardinality of bags *) `````` Jean-Christophe Filliatre committed Apr 16, 2012 82 83 84 `````` function card (bag 'a): int `````` Mário Pereira committed Jul 09, 2015 85 `````` axiom Card_nonneg: forall x: bag 'a. card x >= 0 `````` Jean-Christophe Filliatre committed Apr 16, 2012 86 87 88 89 90 91 92 `````` axiom Card_empty: card (empty_bag: bag 'a) = 0 axiom Card_zero_empty: forall x: bag 'a. card x = 0 -> x = empty_bag axiom Card_singleton: forall x:'a. card (singleton x) = 1 axiom Card_union: forall x y: bag 'a. card (union x y) = card x + card y lemma Card_add: forall x: 'a, b: bag 'a. card (add x b) = 1 + card b `````` MARCHE Claude committed Apr 19, 2012 93 `````` (** bag difference *) `````` Jean-Christophe Filliatre committed Apr 16, 2012 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 `````` use import int.MinMax function diff (bag 'a) (bag 'a) : bag 'a axiom Diff_occ: forall b1 b2: bag 'a, x:'a. nb_occ x (diff b1 b2) = max 0 (nb_occ x b1 - nb_occ x b2) lemma Diff_empty_right: forall b: bag 'a. diff b empty_bag = b lemma Diff_empty_left: forall b: bag 'a. diff empty_bag b = empty_bag lemma Diff_add: forall b: bag 'a, x:'a. diff (add x b) (singleton x) = b lemma Diff_comm: forall b b1 b2: bag 'a. diff (diff b b1) b2 = diff (diff b b2) b1 lemma Add_diff: forall b: bag 'a, x:'a. mem x b -> add x (diff b (singleton x)) = b `````` Mário Pereira committed Jul 09, 2015 113 114 115 116 117 118 119 `````` (** arbitrary element *) function choose (b: bag 'a) : 'a axiom choose_mem: forall b: bag 'a. empty_bag <> b -> mem (choose b) b `````` Jean-Christophe Filliatre committed Apr 16, 2012 120 ``end``