| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/structures/ (Columbo Version 0.7©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle bags_aux.pvs Sprache: PVS |
|||||||||
|
bags_aux[T:TYPE]:THEORY
%------------------------------------------------------------------------ % % Additional properties about bags % % Author: David Griffioen (CWI Amsterdam and KUN) % %------------------------------------------------------------------------ BEGIN IMPORTING bags[T], bags_to_sets[T] x,y,e: VAR T b: VAR bag n,xn: VAR nat p,q: VAR pred[T] %% ===== choose and rest for bags ===== choose(b: (nonempty_bag?)):T = choose(bag_to_set(b)) rest(b):bag = IF empty?(b) THEN b ELSE delete(choose(b),b,1) ENDIF choose_gt_zero: LEMMA nonempty_bag?(b) => b(choose(b)) > 0 insert_choose_rest: LEMMA nonempty_bag?(b) => insert(choose(b),rest(b)) = b %% ===== on filters ===== % Definition of filter for bags, it takes a bag and a predicate and % returns the bag of those elements that satisfy the predicate. filter(b,p):bag = (LAMBDA x: IF p(x) THEN b(x) ELSE 0 ENDIF) filter_emptybag: THEOREM filter(emptybag,p) = emptybag filter_insert: LEMMA filter(insert(x,b),p) = IF p(x) THEN insert(x,filter(b,p)) ELSE filter(b,p) ENDIF filter_delete: LEMMA filter(delete(x,b,n),p) = delete(x,filter(b,p),n) filter_prop: LEMMA (FORALL x: p(x) => q(x)) => subbag?(filter(b,p),filter(b,q)) END bags_aux ¤ Dauer der Verarbeitung: 0.24 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28