Quellcode-Bibliothek cauchy_scaf.pvs

%%-------------------** Fundamental Counting Principle and Permutations with Repetition  **-------------
%%                                                                          
%% Author          : André Luiz Galdino 
%%                   Universidade Federal de Goiás - Brasil
%%                    
%% Last Modified On: November 28, 2011
%%                                                                          
%%------------------------------------------------------------------------------------------------------


cauchy_scaf[T:TYPE]: THEORY

BEGIN


   IMPORTING structures@seq_extras[T],
             finite_sets@finite_sets_eq,
             finite_sets@finite_sets_card_eq

       S: VAR finite_set[finseq]
       M: VAR finite_set[T]
       a: VAR T
       n: VAR nat
       p: VAR posnat

  
 add_element(S)(a): set[finseq] = {seq: finseq | EXISTS (s: (S)): seq = add_first(a, s)}

 add_set(S)(M): setofsets[finseq] = {C: set[finseq] | EXISTS (a: (M)): C = add_element(S)(a)}

 set_seq(M)(n): set[finseq] = {seq: finseq | length(seq) = n AND 
                                             FORALL (i: below[n]): member(seq(i), M)}


 emptyset_gives_emptyset: LEMMA empty?(S) IMPLIES empty?(add_element(S)(a))

 emptyset_gives_emptyset1: LEMMA empty?(M) IMPLIES empty?(add_set(S)(M))

 set_seq_singleton: LEMMA set_seq(M)(0) = singleton(empty_seq)

 set_seq_empty: LEMMA  empty?(M) IMPLIES empty?(set_seq(M)(p))

 add_element_add_set: LEMMA NOT member(a, M) IMPLIES 
                        LET B = add_set(S)(M),
                            A = add_element(S)(a) IN
                        Union(add_set(S)(add(a, M)))= union(Union(B), A)

 card_add_element_aux: LEMMA 
                         LET A = add_element(S)(a) IN
                         EXISTS (g:[(A)->(S)]): bijective?(g)


 card_add_element: LEMMA 
                         LET A = add_element(S)(a) IN
                         card(A) = card(S)
 
 disjoint_add_set: LEMMA 
                     LET B = add_set(S)(M),
                         A = add_element(S)(a) IN
                       NOT member(a, M) IMPLIES disjoint?(Union(B),A)

 add_set_is_add_ele: LEMMA 
                       LET B = add_set(S)(M),
                           A = add_element(S)(a) IN
                       M = singleton(a) IMPLIES Union(B) = A

 add_set_is_finite_aux: LEMMA
                         nonempty?(S) IMPLIES
                            LET B = add_set(S)(M) IN
                            EXISTS (g:[(M)->(B)]): bijective?(g)

 add_set_is_finite: LEMMA
                     LET B = add_set(S)(M) IN
                     is_finite(B)

%%%%% Fundamental Counting Principle %%%%%

 card_add_set: LEMMA 
                  LET B = add_set(S)(M) IN
                  card(Union(B)) = card(S)*card(M)


 set_seq_is_finite: LEMMA 
                      LET C = set_seq(M)(n) IN
                      is_finite(C)

 set_seq_is_add_set: LEMMA 
                        LET C = set_seq(M)(p),
                            D = set_seq(M)(p-1) IN
                        C = Union(add_set(D)(M))

%%%%% Permutations with Repetition %%%%%

 card_set_seq: LEMMA 
                    LET C = set_seq(M)(n) IN
                    card(C) = card(M)^n

END cauchy_scaf